Index: doc/theses/andrew_beach_MMath/existing.tex
===================================================================
--- doc/theses/andrew_beach_MMath/existing.tex	(revision 1c1c180bbabe89afcd516b9eec10021a2e52dd6b)
+++ doc/theses/andrew_beach_MMath/existing.tex	(revision 29c9b238348fc96b3f7b9cfb6a76d90dcb71b892)
@@ -1,3 +1,3 @@
-\chapter{\texorpdfstring{\CFA Existing Features}{Cforall Existing Features}}
+\chapter{\CFA Existing Features}
 
 \CFA (C-for-all)~\cite{Cforall} is an open-source project extending ISO C with
@@ -43,5 +43,5 @@
 
 \section{Reference Type}
-\CFA adds a rebindable reference type to C, but more expressive than the \CC
+\CFA adds a rebindable reference type to C, but more expressive than the \Cpp
 reference.  Multi-level references are allowed and act like auto-dereferenced
 pointers using the ampersand (@&@) instead of the pointer asterisk (@*@). \CFA
@@ -60,7 +60,7 @@
 
 Both constructors and destructors are operators, which means they are just
-functions with special operator names rather than type names in \CC. The
+functions with special operator names rather than type names in \Cpp. The
 special operator names may be used to call the functions explicitly (not
-allowed in \CC for constructors).
+allowed in \Cpp for constructors).
 
 In general, operator names in \CFA are constructed by bracketing an operator
@@ -89,5 +89,5 @@
 matching overloaded destructor @void ^?{}(T &);@ is called.  Without explicit
 definition, \CFA creates a default and copy constructor, destructor and
-assignment (like \CC). It is possible to define constructors/destructors for
+assignment (like \Cpp). It is possible to define constructors/destructors for
 basic and existing types.
 
@@ -95,5 +95,5 @@
 \CFA uses parametric polymorphism to create functions and types that are
 defined over multiple types. \CFA polymorphic declarations serve the same role
-as \CC templates or Java generics. The ``parametric'' means the polymorphism is
+as \Cpp templates or Java generics. The ``parametric'' means the polymorphism is
 accomplished by passing argument operations to associate \emph{parameters} at
 the call site, and these parameters are used in the function to differentiate
@@ -135,5 +135,5 @@
 
 Note, a function named @do_once@ is not required in the scope of @do_twice@ to
-compile it, unlike \CC template expansion. Furthermore, call-site inferencing
+compile it, unlike \Cpp template expansion. Furthermore, call-site inferencing
 allows local replacement of the most specific parametric functions needs for a
 call.
@@ -179,5 +179,5 @@
 }
 \end{cfa}
-The generic type @node(T)@ is an example of a polymorphic-type usage.  Like \CC
+The generic type @node(T)@ is an example of a polymorphic-type usage.  Like \Cpp
 templates usage, a polymorphic-type usage must specify a type parameter.
 
Index: doc/theses/andrew_beach_MMath/features.tex
===================================================================
--- doc/theses/andrew_beach_MMath/features.tex	(revision 1c1c180bbabe89afcd516b9eec10021a2e52dd6b)
+++ doc/theses/andrew_beach_MMath/features.tex	(revision 29c9b238348fc96b3f7b9cfb6a76d90dcb71b892)
@@ -5,10 +5,24 @@
 
 \section{Virtuals}
+Virtual types and casts are not part of the exception system nor are they
+required for an exception system. But an object-oriented style hierarchy is a
+great way of organizing exceptions so a minimal virtual system has been added
+to \CFA.
+
+The pattern of a simple hierarchy was borrowed from object-oriented
+programming was chosen for several reasons.
+The first is that it allows new exceptions to be added in user code
+and in libraries independently of each other. Another is it allows for
+different levels of exception grouping (all exceptions, all IO exceptions or
+a particular IO exception). Also it also provides a simple way of passing
+data back and forth across the throw.
+
 Virtual types and casts are not required for a basic exception-system but are
 useful for advanced exception features. However, \CFA is not object-oriented so
 there is no obvious concept of virtuals. Hence, to create advanced exception
-features for this work, I needed to designed and implemented a virtual-like
+features for this work, I needed to design and implement a virtual-like
 system for \CFA.
 
+% NOTE: Maybe we should but less of the rational here.
 Object-oriented languages often organized exceptions into a simple hierarchy,
 \eg Java.
@@ -61,13 +75,14 @@
 While much of the virtual infrastructure is created, it is currently only used
 internally for exception handling. The only user-level feature is the virtual
-cast, which is the same as the \CC \lstinline[language=C++]|dynamic_cast|.
+cast, which is the same as the \Cpp \lstinline[language=C++]|dynamic_cast|.
 \label{p:VirtualCast}
 \begin{cfa}
 (virtual TYPE)EXPRESSION
 \end{cfa}
-Note, the syntax and semantics matches a C-cast, rather than the unusual \CC
-syntax for special casts. Both the type of @EXPRESSION@ and @TYPE@ must be a
-pointer to a virtual type. The cast dynamically checks if the @EXPRESSION@ type
-is the same or a subtype of @TYPE@, and if true, returns a pointer to the
+Note, the syntax and semantics matches a C-cast, rather than the function-like
+\Cpp syntax for special casts. Both the type of @EXPRESSION@ and @TYPE@ must be
+a pointer to a virtual type.
+The cast dynamically checks if the @EXPRESSION@ type is the same or a subtype
+of @TYPE@, and if true, returns a pointer to the
 @EXPRESSION@ object, otherwise it returns @0p@ (null pointer).
 
@@ -82,23 +97,25 @@
 \begin{cfa}
 trait is_exception(exceptT &, virtualT &) {
-	virtualT const & @get_exception_vtable@(exceptT *);
+	virtualT const & get_exception_vtable(exceptT *);
 };
 \end{cfa}
-The function takes any pointer, including the null pointer, and returns a
-reference to the virtual-table object. Defining this function also establishes
-the virtual type and a virtual-table pair to the \CFA type-resolver and
-promises @exceptT@ is a virtual type and a child of the base exception-type.
-
-\PAB{I do not understand this paragraph.}
-One odd thing about @get_exception_vtable@ is that it should always be a
-constant function, returning the same value regardless of its argument. A
-pointer or reference to the virtual table instance could be used instead,
-however using a function has some ease of implementation advantages and allows
-for easier disambiguation because the virtual type name (or the address of an
-instance that is in scope) can be used instead of the mangled virtual table
-name. Also note the use of the word ``promise'' in the trait
-description. Currently, \CFA cannot check to see if either @exceptT@ or
-@virtualT@ match the layout requirements. This is considered part of
-@get_exception_vtable@'s correct implementation.
+The trait is defined over two types, the exception type and the virtual table
+type. This should be one-to-one, each exception type has only one virtual
+table type and vice versa. The only assertion in the trait is
+@get_exception_vtable@, which takes a pointer of the exception type and
+returns a reference to the virtual table type instance.
+
+The function @get_exception_vtable@ is actually a constant function.
+Recardless of the value passed in (including the null pointer) it should
+return a reference to the virtual table instance for that type.
+The reason it is a function instead of a constant is that it make type
+annotations easier to write as you can use the exception type instead of the
+virtual table type; which usually has a mangled name.
+% Also \CFA's trait system handles functions better than constants and doing
+% it this way
+
+% I did have a note about how it is the programmer's responsibility to make
+% sure the function is implemented correctly. But this is true of every
+% similar system I know of (except Agda's I guess) so I took it out.
 
 \section{Raise}
@@ -109,5 +126,5 @@
 trait is_termination_exception(
 		exceptT &, virtualT & | is_exception(exceptT, virtualT)) {
-	void @defaultTerminationHandler@(exceptT &);
+	void defaultTerminationHandler(exceptT &);
 };
 \end{cfa}
@@ -119,5 +136,5 @@
 trait is_resumption_exception(
 		exceptT &, virtualT & | is_exception(exceptT, virtualT)) {
-	void @defaultResumptionHandler@(exceptT &);
+	void defaultResumptionHandler(exceptT &);
 };
 \end{cfa}
@@ -126,9 +143,18 @@
 
 Finally there are three convenience macros for referring to the these traits:
-@IS_EXCEPTION@, @IS_TERMINATION_EXCEPTION@ and @IS_RESUMPTION_EXCEPTION@. Each
-takes the virtual type's name, and for polymorphic types only, the
-parenthesized list of polymorphic arguments. These macros do the name mangling
-to get the virtual-table name and provide the arguments to both sides
-\PAB{What's a ``side''?}
+@IS_EXCEPTION@, @IS_TERMINATION_EXCEPTION@ and @IS_RESUMPTION_EXCEPTION@.
+All three traits are hard to use while naming the virtual table as it has an
+internal mangled name. These macros take the exception name as their first
+argument and do the mangling. They all take a second argument for polymorphic
+types which is the parenthesized list of polymorphic arguments. These
+arguments are passed to both the exception type and the virtual table type as
+the arguments do have to match.
+
+For example consider a function that is polymorphic over types that have a
+defined arithmetic exception:
+\begin{cfa}
+forall(Num | IS_EXCEPTION(Arithmetic, (Num)))
+void some_math_function(Num & left, Num & right);
+\end{cfa}
 
 \subsection{Termination}
@@ -147,12 +173,13 @@
 throw EXPRESSION;
 \end{cfa}
-The expression must return a termination-exception reference, where the
-termination exception has a type with a @void defaultTerminationHandler(T &)@
-(default handler) defined. The handler is found at the call site using \CFA's
-trait system and passed into the exception system along with the exception
-itself.
-
-At runtime, a representation of the exception type and an instance of the
-exception type is copied into managed memory (heap) to ensure it remains in
+The expression must return a reference to a termination exception, where the
+termination exception is any type that satifies @is_termination_exception@
+at the call site.
+Through \CFA's trait system the functions in the traits are passed into the
+throw code. A new @defaultTerminationHandler@ can be defined in any scope to
+change the throw's behavior (see below).
+
+At runtime, the exception returned by the expression
+is copied into managed memory (heap) to ensure it remains in
 scope during unwinding. It is the user's responsibility to ensure the original
 exception object at the throw is freed when it goes out of scope. Being
@@ -166,7 +193,7 @@
 try {
 	GUARDED_BLOCK
-} @catch (EXCEPTION_TYPE$\(_1\)$ * NAME)@ { // termination handler 1
+} catch (EXCEPTION_TYPE$\(_1\)$ * NAME$\(_1\)$) { // termination handler 1
 	HANDLER_BLOCK$\(_1\)$
-} @catch (EXCEPTION_TYPE$\(_2\)$ * NAME)@ { // termination handler 2
+} catch (EXCEPTION_TYPE$\(_2\)$ * NAME$\(_2\)$) { // termination handler 2
 	HANDLER_BLOCK$\(_2\)$
 }
@@ -179,16 +206,18 @@
 Exception matching checks the representation of the thrown exception-type is
 the same or a descendant type of the exception types in the handler clauses. If
-there is a match, a pointer to the exception object created at the throw is
-bound to @NAME@ and the statements in the associated @HANDLER_BLOCK@ are
-executed. If control reaches the end of the handler, the exception is freed,
-and control continues after the try statement.
+it is the same of a descendent of @EXCEPTION_TYPE@$_i$ then @NAME@$_i$ is
+bound to a pointer to the exception and the statements in @HANDLER_BLOCK@$_i$
+are executed. If control reaches the end of the handler, the exception is
+freed and control continues after the try statement.
 
 The default handler visible at the throw statement is used if no matching
 termination handler is found after the entire stack is searched. At that point,
 the default handler is called with a reference to the exception object
-generated at the throw. If the default handler returns, the system default
-action is executed, which often terminates the program. This feature allows
+generated at the throw. If the default handler returns, control continues
+from after the throw statement. This feature allows
 each exception type to define its own action, such as printing an informative
 error message, when an exception is not handled in the program.
+However the default handler for all exception types triggers a cancellation
+using the exception.
 
 \subsection{Resumption}
@@ -197,6 +226,6 @@
 Resumption raise, called ``resume'', is as old as termination
 raise~\cite{Goodenough75} but is less popular. In many ways, resumption is
-simpler and easier to understand, as it is simply a dynamic call (as in
-Lisp). The semantics of resumption is: search the stack for a matching handler,
+simpler and easier to understand, as it is simply a dynamic call.
+The semantics of resumption is: search the stack for a matching handler,
 execute the handler, and continue execution after the resume. Notice, the stack
 cannot be unwound because execution returns to the raise point. Resumption is
@@ -210,12 +239,13 @@
 \end{cfa}
 The semantics of the @throwResume@ statement are like the @throw@, but the
-expression has a type with a @void defaultResumptionHandler(T &)@ (default
-handler) defined, where the handler is found at the call site by the type
-system. At runtime, a representation of the exception type and an instance of
-the exception type is \emph{not} copied because the stack is maintained during
-the handler search.
+expression has return a reference a type that satifies the trait
+@is_resumption_exception@. Like with termination the exception system can
+use these assertions while (throwing/raising/handling) the exception.
+
+At runtime, no copies are made. As the stack is not unwound the exception and
+any values on the stack will remain in scope while the resumption is handled.
 
 Then the exception system searches the stack starting from the resume and
-proceeding towards the base of the stack, from callee to caller. At each stack
+proceeding to the base of the stack, from callee to caller. At each stack
 frame, a check is made for resumption handlers defined by the @catchResume@
 clauses of a @try@ statement.
@@ -223,7 +253,7 @@
 try {
 	GUARDED_BLOCK
-} @catchResume (EXCEPTION_TYPE$\(_1\)$ * NAME)@ { // resumption handler 1
+} catchResume (EXCEPTION_TYPE$\(_1\)$ * NAME$\(_1\)$) {
 	HANDLER_BLOCK$\(_1\)$
-} @catchResume (EXCEPTION_TYPE$\(_2\)$ * NAME)@ { // resumption handler 2
+} catchResume (EXCEPTION_TYPE$\(_2\)$ * NAME$\(_2\)$) {
 	HANDLER_BLOCK$\(_2\)$
 }
@@ -254,8 +284,8 @@
 current point on the stack because new try statements may have been pushed by
 the handler or functions called from the handler. If there is no match back to
-the point of the current handler, the search skips\label{p:searchskip} the stack frames already
-searched by the first resume and continues after the try statement. The default
-handler always continues from default handler associated with the point where
-the exception is created.
+the point of the current handler, the search skips\label{p:searchskip} the
+stack frames already searched by the first resume and continues after
+the try statement. The default handler always continues from default
+handler associated with the point where the exception is created.
 
 % This might need a diagram. But it is an important part of the justification
@@ -276,7 +306,8 @@
 \end{verbatim}
 
-This resumption search-pattern reflect the one for termination, which matches
-with programmer expectations. However, it avoids the \emph{recursive
-resumption} problem. If parts of the stack are searched multiple times, loops
+This resumption search pattern reflects the one for termination, and so
+should come naturally to most programmers.
+However, it avoids the \emph{recursive resumption} problem.
+If parts of the stack are searched multiple times, loops
 can easily form resulting in infinite recursion.
 
@@ -284,20 +315,23 @@
 \begin{cfa}
 try {
-	throwResume$\(_1\)$ (E &){};
-} catch( E * ) {
-	throwResume;
-}
-\end{cfa}
-Based on termination semantics, programmer expectation is for the re-resume to
-continue searching the stack frames after the try statement. However, the
-current try statement is still on the stack below the handler issuing the
-reresume \see{\VRef{s:Reraise}}. Hence, the try statement catches the re-raise
-again and does another re-raise \emph{ad infinitum}, which is confusing and
-difficult to debug. The \CFA resumption search-pattern skips the try statement
-so the reresume search continues after the try, mathcing programmer
-expectation.
+	throwResume (E &){}; // first
+} catchResume(E *) {
+	throwResume (E &){}; // second
+}
+\end{cfa}
+If this handler is ever used it will be placed on top of the stack above the
+try statement. If the stack was not masked than the @throwResume@ in the
+handler would always be caught by the handler, leading to an infinite loop.
+Masking avoids this problem and other more complex versions of it involving
+multiple handlers and exception types.
+
+Other masking stratagies could be used; such as masking the handlers that
+have caught an exception. This one was choosen because it creates a symmetry
+with termination (masked sections of the stack would be unwound with
+termination) and having only one pattern to learn is easier.
 
 \section{Conditional Catch}
-Both termination and resumption handler-clauses may perform conditional matching:
+Both termination and resumption handler clauses can be given an additional
+condition to further control which exceptions they handle:
 \begin{cfa}
 catch (EXCEPTION_TYPE * NAME ; @CONDITION@)
@@ -323,4 +357,7 @@
 
 \section{Reraise}
+\color{red}{From Andrew: I recomend we talk about why the language doesn't
+have rethrows/reraises instead.}
+
 \label{s:Reraise}
 Within the handler block or functions called from the handler block, it is
@@ -328,5 +365,7 @@
 @throwResume@, respective.
 \begin{cfa}
-catch( ... ) {
+try {
+	...
+} catch( ... ) {
 	... throw; // rethrow
 } catchResume( ... ) {
@@ -341,5 +380,4 @@
 handler is generated that does a program-level abort.
 
-
 \section{Finally Clauses}
 A @finally@ clause may be placed at the end of a @try@ statement.
@@ -347,12 +385,14 @@
 try {
 	GUARDED_BLOCK
-} ...	// any number or kind of handler clauses
-} finally {
+} ... // any number or kind of handler clauses
+... finally {
 	FINALLY_BLOCK
 }
 \end{cfa}
-The @FINALLY_BLOCK@ is executed when the try statement is unwound from the
-stack, \ie when the @GUARDED_BLOCK@ or any handler clause finishes. Hence, the
-finally block is always executed.
+The @FINALLY_BLOCK@ is executed when the try statement is removed from the
+stack, including when the @GUARDED_BLOCK@ or any handler clause finishes or
+during an unwind.
+The only time the block is not executed is if the program is exited before
+that happens.
 
 Execution of the finally block should always finish, meaning control runs off
@@ -370,4 +410,5 @@
 possible forwards the cancellation exception to a different stack.
 
+Cancellation is not an exception operation like termination or resumption.
 There is no special statement for starting a cancellation; instead the standard
 library function @cancel_stack@ is called passing an exception. Unlike a
@@ -379,7 +420,8 @@
 \item[Main Stack:]
 The main stack is the one used by the program main at the start of execution,
-and is the only stack in a sequential program. Hence, when cancellation is
-forwarded to the main stack, there is no other forwarding stack, so after the
-stack is unwound, there is a program-level abort.
+and is the only stack in a sequential program. Even in a concurrent program
+the main stack is only dependent on the environment that started the program.
+Hence, when the main stack is cancelled there is nowhere else in the program
+to notify. After the stack is unwound, there is a program-level abort.
 
 \item[Thread Stack:]
@@ -387,7 +429,8 @@
 @is_thread@ trait. A thread only has two points of communication that must
 happen: start and join. As the thread must be running to perform a
-cancellation, it must occur after start and before join, so join is a
-cancellation point. After the stack is unwound, the thread halts and waits for
-another thread to join with it. The joining thread, checks for a cancellation,
+cancellation, it must occur after start and before join, so join is used
+for communication here.
+After the stack is unwound, the thread halts and waits for
+another thread to join with it. The joining thread checks for a cancellation,
 and if present, resumes exception @ThreadCancelled@.
 
@@ -397,13 +440,16 @@
 the exception is not caught. The implicit join does a program abort instead.
 
-This semantics is for safety. One difficult problem for any exception system is
-defining semantics when an exception is raised during an exception search:
-which exception has priority, the original or new exception? No matter which
-exception is selected, it is possible for the selected one to disrupt or
-destroy the context required for the other. \PAB{I do not understand the
-following sentences.} This loss of information can happen with join but as the
-thread destructor is always run when the stack is being unwound and one
-termination/cancellation is already active. Also since they are implicit they
-are easier to forget about.
+This semantics is for safety. If an unwind is triggered while another unwind
+is underway only one of them can proceed as they both want to ``consume'' the
+stack. Letting both try to proceed leads to very undefined behaviour.
+Both termination and cancellation involve unwinding and, since the default
+@defaultResumptionHandler@ preforms a termination that could more easily
+happen in an implicate join inside a destructor. So there is an error message
+and an abort instead.
+
+The recommended way to avoid the abort is to handle the intial resumption
+from the implicate join. If required you may put an explicate join inside a
+finally clause to disable the check and use the local
+@defaultResumptionHandler@ instead.
 
 \item[Coroutine Stack:] A coroutine stack is created for a @coroutine@ object
Index: doc/theses/andrew_beach_MMath/future.tex
===================================================================
--- doc/theses/andrew_beach_MMath/future.tex	(revision 1c1c180bbabe89afcd516b9eec10021a2e52dd6b)
+++ doc/theses/andrew_beach_MMath/future.tex	(revision 29c9b238348fc96b3f7b9cfb6a76d90dcb71b892)
@@ -10,6 +10,6 @@
 \item
 The implementation of termination is not portable because it includes
-hand-crafted assembly statements. These sections must be generalized to support
-more hardware architectures, \eg ARM processor.
+hand-crafted assembly statements. These sections must be ported by hand to
+support more hardware architectures, such as the ARM processor.
 \item
 Due to a type-system problem, the catch clause cannot bind the exception to a
@@ -24,4 +24,15 @@
 scope of the @try@ statement, where the local control-flow transfers are
 meaningful.
+\item
+There is no detection of colliding unwinds. It is possible for clean-up code
+run during an unwind to trigger another unwind that escapes the clean-up code
+itself; such as a termination exception caught further down the stack or a
+cancellation. There do exist ways to handle this but currently they are not
+even detected and the first unwind will simply be forgotten, often leaving
+it in a bad state.
+\item
+Also the exception system did not have a lot of time to be tried and tested.
+So just letting people use the exception system more will reveal new
+quality of life upgrades that can be made with time.
 \end{itemize}
 
Index: doc/theses/andrew_beach_MMath/uw-ethesis-frontpgs.tex
===================================================================
--- doc/theses/andrew_beach_MMath/uw-ethesis-frontpgs.tex	(revision 1c1c180bbabe89afcd516b9eec10021a2e52dd6b)
+++ doc/theses/andrew_beach_MMath/uw-ethesis-frontpgs.tex	(revision 29c9b238348fc96b3f7b9cfb6a76d90dcb71b892)
@@ -13,20 +13,16 @@
         \vspace*{1.0cm}
 
-        \Huge
-        {\bf Exception Handling in \CFA}
+        {\Huge\bf Exception Handling in \CFA}
 
         \vspace*{1.0cm}
 
-        \normalsize
         by \\
 
         \vspace*{1.0cm}
 
-        \Large
-        Andrew James Beach \\
+        {\Large Andrew James Beach} \\
 
         \vspace*{3.0cm}
 
-        \normalsize
         A thesis \\
         presented to the University of Waterloo \\
@@ -43,5 +39,5 @@
         \vspace*{1.0cm}
 
-        \copyright\ Andrew James Beach \the\year \\
+        \copyright{} Andrew James Beach \the\year \\
         \end{center}
 \end{titlepage}
Index: doc/theses/andrew_beach_MMath/uw-ethesis.tex
===================================================================
--- doc/theses/andrew_beach_MMath/uw-ethesis.tex	(revision 1c1c180bbabe89afcd516b9eec10021a2e52dd6b)
+++ doc/theses/andrew_beach_MMath/uw-ethesis.tex	(revision 29c9b238348fc96b3f7b9cfb6a76d90dcb71b892)
@@ -70,5 +70,5 @@
 %    un-comment the second \documentclass line.
 % 2) change the value assigned below to the boolean variable "PrintVersion"
-%    from " false" to "true".
+%    from "false" to "true".
 
 % ======================================================================
@@ -82,4 +82,6 @@
 % one above:
 %\documentclass[letterpaper,12pt,titlepage,openright,twoside,final]{book}
+
+\usepackage{etoolbox}
 
 % Some LaTeX commands I define for my own nomenclature.
@@ -105,4 +107,6 @@
 % For including graphics N.B. pdftex graphics driver
 \usepackage[pdftex]{graphicx}
+% Removes large sections of the document.
+\usepackage{comment}
 
 % Hyperlinks make it very easy to navigate an electronic document.
@@ -201,11 +205,24 @@
 \makeglossaries
 
-\usepackage{comment}
 % cfa macros used in the document
 %\usepackage{cfalab}
+% I'm going to bring back eventually.
+\makeatletter
+% Combines all \CC* commands:
+\newrobustcmd*\Cpp[1][\xspace]{\cfalab@Cpp#1}
+\newcommand\cfalab@Cpp{C\kern-.1em\hbox{+\kern-.25em+}}
+% Optional arguments do not work with pdf string. (Some fix-up required.)
+\pdfstringdefDisableCommands{\def\Cpp{C++}}
+\makeatother
+
 \input{common}
-\CFAStyle						% CFA code-style for all languages
-\lstset{language=CFA,basicstyle=\linespread{0.9}\tt}	% CFA default lnaguage
+% CFA code-style for all languages
+\CFAStyle
+% CFA default lnaguage
+\lstset{language=CFA,basicstyle=\linespread{0.9}\tt}
+% Annotations from Peter:
 \newcommand{\PAB}[1]{{\color{blue}PAB: #1}}
+% Change the style of abbreviations:
+\renewcommand{\abbrevFont}{}
 
 %======================================================================