Index: doc/theses/andrew_beach_MMath/Makefile
===================================================================
--- doc/theses/andrew_beach_MMath/Makefile	(revision 47e000c054a8dc58293a93fbc643e10735fd30f9)
+++ doc/theses/andrew_beach_MMath/Makefile	(revision de47a9d90448b4a9998ca306ff8576f8cd4f3369)
@@ -1,34 +1,30 @@
 ### Makefile for Andrew Beach's Masters Thesis
 
-DOC = uw-ethesis.pdf
-BASE = ${DOC:%.pdf=%} # remove suffix
-# directory for latex clutter files
-BUILD = build
-TEXSRC = $(wildcard *.tex)
-FIGSRC = $(wildcard *.fig)
-BIBSRC = $(wildcard *.bib)
-STYSRC = $(wildcard *.sty)
-CLSSRC = $(wildcard *.cls)
-TEXLIB = .:../../LaTeXmacros:${BUILD}: # common latex macros
-BIBLIB = .:../../bibliography # common citation repository
+DOC=uw-ethesis.pdf
+BUILD=out
+TEXSRC=$(wildcard *.tex)
+BIBSRC=$(wildcard *.bib)
+STYSRC=$(wildcard *.sty)
+CLSSRC=$(wildcard *.cls)
+TEXLIB= .:../../LaTeXmacros:${BUILD}:
+BIBLIB= .:../../bibliography
 
-MAKEFLAGS = --no-print-directory # --silent
-VPATH = ${BUILD}
+# Since tex programs like to add their own file extensions:
+BASE= ${DOC:%.pdf=%}
 
 ### Special Rules:
 
 .PHONY: all clean deepclean
-.PRECIOUS: %.dvi %.ps # do not delete intermediate files
 
 ### Commands:
-LATEX = TEXINPUTS=${TEXLIB} && export TEXINPUTS && latex -halt-on-error -output-directory=${BUILD}
-BIBTEX = BIBINPUTS=${BIBLIB} bibtex
-GLOSSARY = INDEXSTYLE=${BUILD} makeglossaries-lite
+LATEX=TEXINPUTS=${TEXLIB} pdflatex -halt-on-error -output-directory=${BUILD}
+BIBTEX=BIBINPUTS=${BIBLIB} bibtex
+GLOSSARY=INDEXSTYLE=${BUILD} makeglossaries-lite
 
-### Rules and Recipes:
+### Rules and Recipies:
 
 all: ${DOC}
 
-${BUILD}/%.dvi: ${TEXSRC} ${FIGSRC:.fig=.tex} ${BIBSRC} ${STYSRC} ${CLSSRC} Makefile | ${BUILD}
+${BUILD}/${DOC}: ${TEXSRC} ${BIBSRC} ${STYSRC} ${CLSSRC} Makefile | ${BUILD}
 	${LATEX} ${BASE}
 	${BIBTEX} ${BUILD}/${BASE}
@@ -37,26 +33,13 @@
 	${LATEX} ${BASE}
 
+${DOC}: ${BUILD}/${DOC}
+	cp $< $@
+
 ${BUILD}:
 	mkdir $@
 
-%.pdf : ${BUILD}/%.ps | ${BUILD}
-	ps2pdf $<
-
-%.ps : %.dvi | ${BUILD}
-	dvips $< -o $@
-
-%.tex : %.fig | ${BUILD}
-	fig2dev -L eepic $< > ${BUILD}/$@
-
-%.ps : %.fig | ${BUILD}
-	fig2dev -L ps $< > ${BUILD}/$@
-
-%.pstex : %.fig | ${BUILD}
-	fig2dev -L pstex $< > ${BUILD}/$@
-	fig2dev -L pstex_t -p ${BUILD}/$@ $< > ${BUILD}/$@_t
-
 clean:
-	@rm -frv ${BUILD} *.fig.bak
+	-@rm -rv ${BUILD}
 
 deepclean: clean
-	-@rm -fv ${DOC}
+	-@rm -v ${DOC}
Index: doc/theses/andrew_beach_MMath/exceptionHierarchy.fig
===================================================================
--- doc/theses/andrew_beach_MMath/exceptionHierarchy.fig	(revision 47e000c054a8dc58293a93fbc643e10735fd30f9)
+++ 	(revision )
@@ -1,28 +1,0 @@
-#FIG 3.2  Produced by xfig version 3.2.7b
-Landscape
-Center
-Inches
-Letter
-100.00
-Single
--2
-1200 2
-6 3600 2027 3825 2522
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
-	1 1 1.00 45.00 90.00
-	 3600 2050 3825 2050
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3
-	1 1 1.00 45.00 90.00
-	 3675 2050 3675 2275 3825 2275
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3
-	1 1 1.00 45.00 90.00
-	 3675 2275 3675 2500 3825 2500
--6
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
-	1 1 1.00 45.00 90.00
-	 2175 2050 2400 2050
-4 1 0 50 -1 5 12 0.0000 2 120 1200 3000 2100 arithmetic\001
-4 2 0 50 -1 5 12 0.0000 2 165 1080 2100 2100 exception\001
-4 0 0 50 -1 5 12 0.0000 2 120 1080 3900 2100 underflow\001
-4 0 0 50 -1 5 12 0.0000 2 120 960 3900 2325 overflow\001
-4 0 0 50 -1 5 12 0.0000 2 120 1200 3900 2550 zerodivide\001
Index: doc/theses/andrew_beach_MMath/features.tex
===================================================================
--- doc/theses/andrew_beach_MMath/features.tex	(revision 47e000c054a8dc58293a93fbc643e10735fd30f9)
+++ doc/theses/andrew_beach_MMath/features.tex	(revision de47a9d90448b4a9998ca306ff8576f8cd4f3369)
@@ -3,7 +3,4 @@
 This chapter covers the design and user interface of the \CFA
 exception-handling mechanism (EHM). % or exception system.
-While an EHM is free to add many features,
-the following overview covers the basic features that all EHMs use, but it is not an
-exhaustive list of everything an EHM can do.
 
 % We should cover what is an exception handling mechanism and what is an
@@ -12,78 +9,90 @@
 \paragraph{Raise / Handle}
 An exception operation has two main parts: raise and handle.
+These are the two parts that the user will write themselves and so
+might be the only two pieces of the EHM that have any syntax.
 These terms are sometimes also known as throw and catch but this work uses
 throw/catch as a particular kind of raise/handle.
-These are the two parts a programmer writes and so
-are the only two pieces of the EHM that have language syntax.
 
 \subparagraph{Raise}
-The raise is the starting point for exception handling and usually how \PAB{This sentence is cut off.}
-Some well known examples include the @throw@ statement of \Cpp and Java and
-the \lstinline[language=Python]{raise} statement from Python.
-
-For this overview, a raise starts the handling of an
-exception, which is called \newterm{raising} an exception. This simple description is sufficient
-for the overview.
+The raise is the starting point for exception handling and usually how
+Some well known examples include the throw statements of \Cpp and Java and
+the raise statement from Python.
+
+For this overview a raise does nothing more kick off the handling of an
+exception, which is called raising the exception. This is inexact but close
+enough for the broad strokes of the overview.
 
 \subparagraph{Handle}
-The purpose of raising an exception is to run user code to address (handle) the
-issue found at the raise point.
-The @try@ statement of \Cpp illustrates a common approach for specifying multiple handlers.
-A handler has three common features: the scope in which it applies, an
-exception label that describes what exceptions it can handle, and code to run
-that deals with the raised issue.
-Each handler can handle exceptions raised in the region matching its
-exception label. For multiple matches, different EHMs have different rules for matching an exception to a handler label,
-such as ``best match" or ``first found".
+The purpose of most exception operations is to run some sort of handler that
+contains user code.
+The try statement of \Cpp illistrates the common features
+Handlers have three common features: a region of code they apply to, an
+exception label that describes what exceptions they handle and code to run
+when they handle an exception.
+Each handler can handle exceptions raised in that region that match their
+exception label. Different EHMs will have different rules to pick a handler
+if multipe handlers could be used such as ``best match" or ``first found".
 
 \paragraph{Propagation}
-After an exception is raised, comes the most complex step for the
-EHM: finding and setting up the handler. This propagation of exception from raise to handler can be broken up into three
-different tasks: searching, matching, and
-installing the handler so it can execute.
-
-\subparagraph{Searching}
-The EHM searches for possible handlers that can be used to handle
-the exception. Searching is usually independent of the exception that is
-thrown and instead depends on the call stack: current function, its caller
+After an exception is raised comes what is usually the biggest step for the
+EHM, finding and setting up the handler. This can be broken up into three
+different tasks: searching for a handler, matching against the handler and
+installing the handler.
+
+First the EHM must search for possible handlers that could be used to handle
+the exception. Searching is usually independent of the exception that was
+thrown and instead depends on the call stack, the current function, its caller
 and repeating down the stack.
 
-\subparagraph{Matching}
-For each handler found, it compares the raised exception with the handler label to see which one is the
-best match, and hence, which one should be used to handle the exception.
-In languages where the best match is the first match, these two steps are often
-intertwined, \ie a match check is performed immediately after the search finds
+Second it much match the exception with each handler to see which one is the
+best match and hence which one should be used to handle the exception.
+In languages where the best match is the first match these two are often
+intertwined, a match check is preformed immediately after the search finds
 a possible handler.
 
-\subparagraph{Installing}
-After a handler is chosen, it must be made ready to run.
-This step varies widely to fit with the rest of the
-design of the EHM. The installation step might be trivial or it can be
+Third, after a handler is chosen it must be made ready to run.
+What this actually involves can vary widely to fit with the rest of the
+design of the EHM. The installation step might be trivial or it could be
 the most expensive step in handling an exception. The latter tends to be the
 case when stack unwinding is involved.
-An alternate action occurs if no appropriate handler is found, then some implicit action
-is performed. This step is only required with unchecked
-exceptions as checked exceptions (Java) promise a handler is always found. The implicit action
-also installs a handler but it is a default handle that may be
+
+As an alternate third step if no appropriate handler is found then some sort
+of recovery has to be preformed. This is only required with unchecked
+exceptions as checked exceptions can promise that a handler is found. It also
+is also installing a handler but it is a special default that may be
 installed differently.
 
 \subparagraph{Hierarchy}
-Some EHM (\CFA, Java) organize exceptions in a hierarchical structure.
-This strategy is borrowed from object-orientated languages where the
+In \CFA the EHM uses a hierarchial system to organise its exceptions.
+This stratagy is borrowed from object-orientated languages where the
 exception hierarchy is a natural extension of the object hierarchy.
 
 Consider the following hierarchy of exceptions:
 \begin{center}
-\input{exceptionHierarchy}
+\setlength{\unitlength}{4000sp}%
+\begin{picture}(1605,612)(2011,-1951)
+\put(2100,-1411){\vector(1, 0){225}}
+\put(3450,-1411){\vector(1, 0){225}}
+\put(3550,-1411){\line(0,-1){225}}
+\put(3550,-1636){\vector(1, 0){150}}
+\put(3550,-1636){\line(0,-1){225}}
+\put(3550,-1861){\vector(1, 0){150}}
+\put(2025,-1490){\makebox(0,0)[rb]{\LstBasicStyle{exception}}}
+\put(2400,-1460){\makebox(0,0)[lb]{\LstBasicStyle{arithmetic}}}
+\put(3750,-1460){\makebox(0,0)[lb]{\LstBasicStyle{underflow}}}
+\put(3750,-1690){\makebox(0,0)[lb]{\LstBasicStyle{overflow}}}
+\put(3750,-1920){\makebox(0,0)[lb]{\LstBasicStyle{zerodivide}}}
+\end{picture}%
 \end{center}
+
 A handler labelled with any given exception can handle exceptions of that
 type or any child type of that exception. The root of the exception hierarchy
-(here \lstinline[language=C++]{exception}) acts as a catch-all, leaf types catch single types
+(here \texttt{exception}) acts as a catch-all, leaf types catch single types
 and the exceptions in the middle can be used to catch different groups of
 related exceptions.
 
 This system has some notable advantages, such as multiple levels of grouping,
-the ability for libraries to add new exception types, and the isolation
-between different sub-hierarchies. This capability had to be adapted for \CFA, which is a
+the ability for libraries to add new exception types and the isolation
+between different sub-hierarchies. So the design was adapted for a
 non-object-orientated language.
 
@@ -91,26 +100,34 @@
 
 \paragraph{Completion}
-After the handler has returned, the entire exception operation has to complete
-and continue executing somewhere. This step is usually simple,
-both logically and in its implementation, as the installation of the handler
-usually does the preparation.
-The EHM can return control to different places,
-where the most common are after the handler definition or after the raise.
+After the handler has finished the entire exception operation has to complete
+and continue executing somewhere else. This step is usually very simple
+both logically and in its implementation as the installation of the handler
+usually does the heavy lifting.
+
+The EHM can return control to many different places.
+However, the most common is after the handler definition and the next most
+common is after the raise.
 
 \paragraph{Communication}
-For effective exception handling, additional information is usually passed from the raise,
-where this basic model only communicates the exception's identity. A common
-methods for communication is putting fields into an exception and
-allowing a handler to access these fields via an exception instance in the handler's scope.
+For effective exception handling, additional information is usually required
+as this base model only communicates the exception's identity. Common
+additional methods of communication are putting fields on an exception and
+allowing a handler to access the lexical scope it is defined in (usually
+a function's local variables).
+
+\paragraph{Other Features}
+Any given exception handling mechanism is free at add other features on top
+of this. This is an overview of the base that all EHMs use but it is not an
+exaustive list of everything an EHM can do.
 
 \section{Virtuals}
-Virtual types and casts are not part of an EHM nor are they
-required for an EHM. But as pointed out, an object-oriented-style hierarchy is an
-excellent way of organizing exceptions. Hence, a minimal virtual system has been added
-to \CFA to support hierarchical exceptions.
+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 virtual system supports multiple ``trees" of types. Each tree is
 a simple hierarchy with a single root type. Each type in a tree has exactly
-one parent -- except for the root type with zero parents -- and any
+one parent - except for the root type which has zero parents - and any
 number of children.
 Any type that belongs to any of these trees is called a virtual type.
@@ -118,33 +135,34 @@
 % A type's ancestors are its parent and its parent's ancestors.
 % The root type has no ancestors.
-% A type's descendents are its children and its children's descendents.
-
-Every virtual type has a list of virtual members. Children inherit
-their parent's virtual members but may add new members to it.
-It is important to note that these are virtual members, not virtual methods of an object type.
-However, as \CFA has function pointers, they can be used to mimic virtual
-methods.
-
-Each virtual type has a unique id.
-The unique id for the virtual type and all its virtual members are combined
-into a virtual-table type. Each virtual type has a pointer to a virtual table
+% A type's decendents are its children and its children's decendents.
+
+Every virtual type also has a list of virtual members. Children inherit
+their parent's list of virtual members but may add new members to it.
+It is important to note that these are virtual members, not virtual methods.
+However as function pointers are allowed they can be used to mimic virtual
+methods as well.
+
+The unique id for the virtual type and all the virtual members are combined
+into a virtual table type. Each virtual type has a pointer to a virtual table
 as a hidden field.
 
-Up to this point, a virtual system is similar to ones found in object-oriented
-languages but this is where \CFA diverges. Objects encapsulate a
+Up until this point the virtual system is a lot like ones found in object-
+orientated languages but this where they diverge. Objects encapsulate a
 single set of behaviours in each type, universally across the entire program,
-and indeed all programs that use that type definition. In this sense, the
+and indeed all programs that use that type definition. In this sense the
 types are ``closed" and cannot be altered.
-However, \CFA types do not encapsulate any behaviour. Instead, traits are used and
-types can satisfy a trait, stop satisfying a trait, or satisfy the same
-trait in a different way depending on the lexical context. In this sense, the types are
-``open" as their behaviour can change in different scopes. This capability means it is impossible to pick
-a single set of functions that represent the type's virtual members.
-
-Hence, \CFA does not have a single virtual table for a type. A user can define different virtual tables,
-which are filled in at their declaration and given a name. 
-That name is used as the virtual table, even if it is defined locally
-inside a function, although lifetime issues must be considered.
-Specifically, an object of a virtual type is ``bound" to a virtual table instance, which
+
+However in \CFA types do not encapsulate any behaviour. Traits are local and
+types can begin to statify a trait, stop satifying a trait or satify the same
+trait in a different way with each new definition. In this sense they are
+``open" as they can change at any time. This means it is implossible to pick
+a single set of functions that repersent the type.
+
+So we don't try to have a single value. The user can define virtual tables
+which are filled in at their declaration and given a name. Anywhere you can
+see that name you can use that virtual table; even if it is defined locally
+inside a function, although in that case you must respect its lifetime.
+
+An object of a virtual type is ``bound" to a virtual table instance which
 sets the virtual members for that object. The virtual members can be accessed
 through the object.
@@ -160,5 +178,5 @@
 \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
+The cast dynamically checks if the @EXPRESSION@ type is the same or a sub-type
 of @TYPE@, and if true, returns a pointer to the
 @EXPRESSION@ object, otherwise it returns @0p@ (null pointer).
@@ -178,15 +196,15 @@
 \end{cfa}
 The trait is defined over two types, the exception type and the virtual table
-type. These type should have a one-to-one relationship: each exception type has only one virtual
+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.
+returns a reference to the virtual table type instance.
 
 The function @get_exception_vtable@ is actually a constant function.
-Regardless of the value passed in (including the null pointer) it
-returns a reference to the virtual-table instance for that type.
-The reason it is a function instead of a constant is to make type
-annotations easier to write using the exception type rather than the
-virtual-table type, which usually has a mangled name because it is an internal component of the EHM.
+Regardless 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 reduce the amount of boiler plate we need.
@@ -194,7 +212,9 @@
 % 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 Ada's I guess) so I took it out.
-
-There are two more exception traits defined as follows:
+% similar system I know of (except Agda's I guess) so I took it out.
+
+There are two more traits for exceptions @is_termination_exception@ and
+@is_resumption_exception@. They are defined as follows:
+
 \begin{cfa}
 trait is_termination_exception(
@@ -208,21 +228,23 @@
 };
 \end{cfa}
-These traits ensure a given type and virtual type are an
-exception type and defines one of the two default handlers. The default handlers
-are used in the main exception-handling operations and discussed in detail in \VRef{s:ExceptionHandling}.
-
-However, all three of these traits are tricky to use directly.
-While there is a bit of repetition required,
-the largest issue is that the virtual-table type is mangled and not in a user
-facing way. So three macros are provided to wrap these traits
-to simplify referring to the names:
+
+In other words they make sure that a given type and virtual type is an
+exception and defines one of the two default handlers. These default handlers
+are used in the main exception handling operations \see{Exception Handling}
+and their use will be detailed there.
+
+However all three of these traits can be tricky to use directly.
+There is a bit of repetition required but
+the largest issue is that the virtual table type is mangled and not in a user
+facing way. So there are three macros that can be used to wrap these traits
+when you need to refer to the names:
 @IS_EXCEPTION@, @IS_TERMINATION_EXCEPTION@ and @IS_RESUMPTION_EXCEPTION@.
 
-These macros take one or two arguments. The first argument is the name of the
-exception type. The macro passes the unmangled and mangled form to the trait.
+All take one or two arguments. The first argument is the name of the
+exception type. Its unmangled and mangled form are passed to the trait.
 The second (optional) argument is a parenthesized list of polymorphic
-arguments. This argument is only used with polymorphic exceptions and the
-list is passed to both types.
-In the current set-up, the base name and the polymorphic arguments have to
+arguments. This argument should only with polymorphic exceptions and the
+list will be passed to both types.
+In the current set-up the base name and the polymorphic arguments have to
 match so these macros can be used without losing flexibility.
 
@@ -230,130 +252,119 @@
 defined arithmetic exception:
 \begin{cfa}
-forall(Num | @IS_EXCEPTION(Arithmetic, Num)@)
+forall(Num | IS_EXCEPTION(Arithmetic, (Num)))
 void some_math_function(Num & left, Num & right);
 \end{cfa}
-where the function may raise exception @Arithmetic@ or any of its decedents.
 
 \section{Exception Handling}
-\label{s:ExceptionHandling}
-\CFA provides two kinds of exception handling: termination and resumption.
-These twin mechanisms are the core of the \CFA EHM and
-multiple features are provided to support them.
-This section covers the general patterns shared by the two kinds of exceptions and
-then covers the individual detail operations.
-
-Both mechanisms follow the same set of steps to do their operations. Both
-start with the user performing an exception raise.
-Then there is the handler search. If one is found, than the exception
-is caught and the handler is run. When the handler returns, control returns to an
-location appropriate for each kind of exception.
-
-\begin{sloppypar}
-If the search fails, an appropriate default handler, @defaultTermiationHandler@
-or @defaultResumptionHandler@, is run and  control returns to the
-appropriate location.
-\end{sloppypar}
+\CFA provides two kinds of exception handling, termination and resumption.
+These twin operations are the core of the exception handling mechanism and
+are the reason for the features of exceptions.
+This section will cover the general patterns shared by the two operations and
+then go on to cover the details each individual operation.
+
+Both operations follow the same set of steps to do their operation. They both
+start with the user preforming a throw on an exception.
+Then there is the search for a handler, if one is found than the exception
+is caught and the handler is run. After that control returns to normal
+execution.
+
+If the search fails a default handler is run and then control
+returns to normal execution immediately. That is where the default handlers
+@defaultTermiationHandler@ and @defaultResumptionHandler@ are used.
 
 \subsection{Termination}
 \label{s:Termination}
-Termination handling is familiar and used in most programming
+
+Termination handling is more familiar kind and used in most programming
 languages with exception handling.
-It is a dynamic, non-local goto. The raise starts searching, and if matched and handled, the stack is
-unwound and control (usually) continues in the function on
-the call stack containing the handler. Terminate is commonly used for an error where recovery
-is impossible in the function performing the raise.
+It is dynamic, non-local goto. If a throw is successful then the stack will
+be unwound and control will (usually) continue in a different function on
+the call stack. They are commonly used when an error has occurred and recovery
+is impossible in the current function.
 
 % (usually) Control can continue in the current function but then a different
 % control flow construct should be used.
 
-A termination raise is started with the @throw@ statement:
+A termination throw is started with the @throw@ statement:
 \begin{cfa}
 throw EXPRESSION;
 \end{cfa}
 The expression must return a reference to a termination exception, where the
-termination exception is any type that satisfies trait
-@is_termination_exception@ at the call site.  Through \CFA's trait system, the
-trait functions are implicitly passed into the hidden throw code and available
-to the exception system while handling the exception. A new
-@defaultTerminationHandler@ can be defined in any scope to change the throw's
-unhandled behaviour (see below).
-
-The throw must copy the provided exception into managed memory because the stack is unwounded.
-The lifetime of the exception copy is managed by the exception runtime.
-It is the user's responsibility to ensure the original exception is cleaned up, where allocating it on the unwound stack is sufficient.
-
-The exception search walks the stack matching with the copied exception.
-It starts from the throwing function and proceeds to the base of the stack,
+termination exception is any type that satisfies @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).
+
+The throw will copy the provided exception into managed memory. It is the
+user's responsibility to ensure the original exception is cleaned up if the
+stack is unwound (allocating it on the stack should be sufficient).
+
+Then the exception system searches the stack using the copied exception.
+It starts starts from the throw and proceeds to the base of the stack,
 from callee to caller.
-At each stack frame, a check is made for termination handlers defined by the
+At each stack frame, a check is made for resumption handlers defined by the
 @catch@ clauses of a @try@ statement.
 \begin{cfa}
 try {
 	GUARDED_BLOCK
-} catch (EXCEPTION_TYPE$\(_1\)$ [* NAME$\(_1\)$]) {
+} catch (EXCEPTION_TYPE$\(_1\)$ * NAME$\(_1\)$) {
 	HANDLER_BLOCK$\(_1\)$
-} catch (EXCEPTION_TYPE$\(_2\)$ [* NAME$\(_2\)$]) {
+} catch (EXCEPTION_TYPE$\(_2\)$ * NAME$\(_2\)$) {
 	HANDLER_BLOCK$\(_2\)$
 }
 \end{cfa}
-When viewed on its own, a @try@ statement with @catch@ clauses simply executes the statements in
-the @GUARDED_BLOCK@, and when those are finished, the try statement finishes.
-
-However, while the guarded statements are being executed, including any invoked
-functions, a termination exception may be thrown. If that exception is not handled by a try
-statement further up the stack, the handlers following the try block are now
-searched for a matching termination exception-type from top to bottom.
-
-Exception matching checks each @catch@ clasue from top to bottom, if the representation of the thrown exception-type is
-the same or a descendant type of the exception types in the @catch@ clauses. If
-it is the same or a descendant of @EXCEPTION_TYPE@$_i$, then the optional @NAME@$_i$ is
+When viewed on its own a try statement will simply execute the statements in
+@GUARDED_BLOCK@ and when those are finished the try statement finishes.
+
+However, while the guarded statements are being executed, including any
+functions they invoke, all the handlers following the try block are now
+or any functions invoked from those
+statements, throws an exception, and the exception
+is not handled by a try statement further up the stack, the termination
+handlers are searched for a matching exception type from top to bottom.
+
+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
+it is the same of a descendant 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.
-
-If no termination handler is found during the search, the default termination
-handler visible at the raise is called.  Through \CFA's trait-system the best
-default-handler match at the throw sight is used.  This function is
-passed the copied exception given to the raise. After the default handler is
-run, control continues after the @throw@ statement.
-
-There is a global @defaultTerminationHandler@ function that that is polymorphic
-over all exception types allowing new default handlers to be defined for
-different exception types and so different exception types can have different
-default handlers.  The global default termination-handler performs a
-cancellation \see{\VRef{s:Cancellation}} on the current stack with the copied
-exception.
+freed and control continues after the try statement.
+
+If no handler is found during the search then the default handler is run.
+Through \CFA's trait system the best match at the throw sight will be used.
+This function is run and is passed the copied exception. After the default
+handler is run control continues after the throw statement.
+
+There is a global @defaultTerminationHandler@ that cancels the current stack
+with the copied exception. However it is generic over all exception types so
+new default handlers can be defined for different exception types and so
+different exception types can have different default handlers.
 
 \subsection{Resumption}
 \label{s:Resumption}
-Resumption exception-handling is a less common counterpart to termination but is
-just as old~\cite{Goodenough75} and is simpler to understand.
-It is a dynamic, non-local function call (like Lisp). If the throw is successful, a
-closure is taken from up the stack and executed, after which the throwing
-function continues executing.
-Resumption is used when an error occurred, and if the error is repaired,
+
+Resumption exception handling is a less common form than termination but is
+just as old~\cite{Goodenough75} and is in some sense simpler.
+It is a dynamic, non-local function call. If the throw is successful a
+closure will be taken from up the stack and executed, after which the throwing
+function will continue executing.
+These are most often used when an error occurred and if the error is repaired
 then the function can continue.
 
-An alternative approach is explicitly passing fixup functions with local
-closures up the stack to be called when an error occurs. However, fixup
-functions significantly expand the parameters list of functions, even when the
-fixup function is not used by a function but must be passed to other called
-functions.
-
 A resumption raise is started with the @throwResume@ statement:
 \begin{cfa}
 throwResume EXPRESSION;
 \end{cfa}
-Like termination, the expression must return a reference to a resumption
-exception, where the resumption exception is any type that satisfies the trait
-@is_termination_exception@ at the call site.
-The assertions for this trait are available to
+The semantics of the @throwResume@ statement are like the @throw@, but the
+expression has return a reference a type that satisfies the trait
+@is_resumption_exception@. The assertions from this trait are available to
 the exception system while handling the exception.
 
-At runtime, no exception copy is made, as the stack is not unwound. Hence, the exception and
-any values on the stack remain in scope while the resumption is handled.
-
-The exception searches walks the stack matching with the provided exception.
-It starts from the resuming function and proceeds to the base of the stack,
+At run-time, 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 using the provided exception.
+It starts starts from the throw and proceeds to the base of the stack,
 from callee to caller.
 At each stack frame, a check is made for resumption handlers defined by the
@@ -362,45 +373,41 @@
 try {
 	GUARDED_BLOCK
-} catchResume (EXCEPTION_TYPE$\(_1\)$ [* NAME$\(_1\)$]) {
+} catchResume (EXCEPTION_TYPE$\(_1\)$ * NAME$\(_1\)$) {
 	HANDLER_BLOCK$\(_1\)$
-} catchResume (EXCEPTION_TYPE$\(_2\)$ [* NAME$\(_2\)$]) {
+} catchResume (EXCEPTION_TYPE$\(_2\)$ * NAME$\(_2\)$) {
 	HANDLER_BLOCK$\(_2\)$
 }
 \end{cfa}
-Termination and resumption handlers may be intermixed in a @try@
-statement but the kind of throw must match with kind of handler for it to be
-considered as a possible match.
-Like termination, when viewed on its own, a @try@ statement with
-@catchResume@ clauses simply executes the statements in the @GUARDED_BLOCK@,
-and when those are finished, the try statement finishes.
-
-However, while the guarded statements are being executed, including any invoked
-functions, a resumption exception may be thrown. If that exception is not handled by a try
-statement further up the stack, the handlers following the try block are now
-searched for a matching resumption exception-type from top to bottom.
-
-Like termination, exception matching checks each @catch@ clasue from top to bottom, if the representation of the thrown exception-type is
-the same or a descendant type of the exception types in the @catchResume@ clauses. If
-it is the same or a descendant of @EXCEPTION_TYPE@$_i$, then the optional @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 @throwResume@ statement.
-
-Like termination, if no resumption handler is found during the search, the
-default resumption handler visible at the raise is called, which is the best
-match at the according to \CFA's overloading rules. This function is passed the
-exception given to the raise. After the default handler is run, execution
-continues after the @throwResume@ statement.
-
-There is a global @defaultResumptionHandler@ that is polymorphic over all
-resumption and preforms a termination throw on the exception.
+If the handlers are not involved in a search this will simply execute the
+@GUARDED_BLOCK@ and then continue to the next statement.
+Its purpose is to add handlers onto the stack.
+(Note, termination and resumption handlers may be intermixed in a @try@
+statement but the kind of throw must be the same as the handler for it to be
+considered as a possible match.)
+
+If a search for a resumption handler reaches a try block it will check each
+@catchResume@ clause, top-to-bottom.
+At each handler if the thrown exception is or is a child type of
+@EXCEPTION_TYPE@$_i$ then the a pointer to the exception is bound to
+@NAME@$_i$ and then @HANDLER_BLOCK@$_i$ is executed. After the block is
+finished control will return to the @throwResume@ statement.
+
+Like termination, if no resumption handler is found, the default handler
+visible at the throw statement is called. It will use the best match at the
+call sight according to \CFA's overloading rules. The default handler is
+passed the exception given to the throw. When the default handler finishes
+execution continues after the throw statement.
+
+There is a global @defaultResumptionHandler@ is polymorphic over all
+termination exceptions and preforms a termination throw on the exception.
 The @defaultTerminationHandler@ for that throw is matched at the original
 throw statement (the resumption @throwResume@) and it can be customized by
 introducing a new or better match as well.
 
-\subsection{Resumption Marking}
+% \subsubsection?
+
 A key difference between resumption and termination is that resumption does
-not unwind the stack. A side effect is that when a handler is matched
-and run its try block (the guarded statements) and every try statement
+not unwind the stack. A side effect that is that when a handler is matched
+and run it's try block (the guarded statements) and every try statement
 searched before it are still on the stack. This can lead to the recursive
 resumption problem.
@@ -416,80 +423,63 @@
 }
 \end{cfa}
-When this code is executed the guarded @throwResume@ starts a
-search and matches the handler in the @catchResume@ clause. The handler is
-called and placed on the stack on top of the try-block. The second throw in the handler
-searches the same try block and calls another instance of the
+When this code is executed the guarded @throwResume@ will throw, start a
+search and match the handler in the @catchResume@ clause. This will be
+call and placed on the stack on top of the try-block. The second throw then
+throws and will search the same try block and put call another instance of the
 same handler leading to an infinite loop.
 
-While this situation is trivial and easy to avoid, much more complex cycles
+This situation is trivial and easy to avoid, but much more complex cycles
 can form with multiple handlers and different exception types.
 
-To prevent this case, examined try statements on the stack are marked, so that
-subsequent resumption searches skip over them and continue with the next unmarked section
-of the stack.
-Unmarking occurs when that exception is handled
-or the search completes without finding a handler.
+To prevent all of these cases we mask sections of the stack, or equivalently
+the try statements on the stack, so that the resumption search skips over
+them and continues with the next unmasked section of the stack.
+
+A section of the stack is marked when it is searched to see if it contains
+a handler for an exception and unmarked when that exception has been handled
+or the search was completed without finding a handler.
 
 % This might need a diagram. But it is an important part of the justification
 % of the design of the traversal order.
-
-\begin{center}
-%\begin{verbatim}
-%       throwResume2 ----------.
-%            |                 |
-% generated from handler       |
-%            |                 |
-%         handler              |
-%            |                 |
-%        throwResume1 -----.   :
-%            |             |   :
-%           try            |   : search skip
-%            |             |   :
-%        catchResume  <----'   :
-%            |                 |
-%\end{verbatim}
-\input{stackMarking}
-\end{center}
-
-The resulting search can be understood by thinking about what is searched for
-termination. When a throw happens in a handler, a termination handler
+\begin{verbatim}
+       throwResume2 ----------.
+            |                 |
+ generated from handler       |
+            |                 |
+         handler              |
+            |                 |
+        throwResume1 -----.   :
+            |             |   :
+           try            |   : search skip
+            |             |   :
+        catchResume  <----'   :
+            |                 |
+\end{verbatim}
+
+The rules can be remembered as thinking about what would be searched in
+termination. So when a throw happens in a handler; a termination handler
 skips everything from the original throw to the original catch because that
-part of the stack is unwound. A resumption handler skips the same
-section of stack because it is marked.
-A throw in a resumption default-handler performs the same search as the original
-@throwResume@ because for resumption nothing has been unwound.
-
-The symmetry between resumption masking and termination searching is why this pattern was picked. Other patterns,
-such as marking just the handlers that caught, also work but the
-symmetry seems to match programmer intuition.
+part of the stack has been unwound, a resumption handler skips the same
+section of stack because it has been masked.
+A throw in a default handler will preform the same search as the original
+throw because; for termination nothing has been unwound, for resumption
+the mask will be the same.
+
+The symmetry with termination is why this pattern was picked. Other patterns,
+such as marking just the handlers that caught, also work but lack the
+symmetry which means there is more to remember.
 
 \section{Conditional Catch}
-Both termination and resumption handler-clauses can be given an additional
-condition to further control which exceptions is handled:
-\begin{cfa}
-catch (EXCEPTION_TYPE [* NAME] @; CONDITION@)
+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)
 \end{cfa}
 First, the same semantics is used to match the exception type. Second, if the
 exception matches, @CONDITION@ is executed. The condition expression may
-reference all names in the scope of the try block and @NAME@
+reference all names in scope at the beginning of the try block and @NAME@
 introduced in the handler clause. If the condition is true, then the handler
 matches. Otherwise, the exception search continues as if the exception type
 did not match.
-
-Conditional catch allows fine-gain matching based on object values as well as exception types.
-For example, assume the exception hierarchy @OpenFailure@ $\rightarrow$ @CreateFailure@ and these exceptions are raised by function @open@.
-\begin{cfa}
-try {
-	f1 = open( ... ); // open raises CreateFailure/OpenFailure
-	f2 = open( ... ); //    with the associate file
-	...
-} catch( CreateFailure * f ; @fd( f ) == f1@ ) {
-	// only handle IO failure for f1
-} catch( OpenFailure * f ; @fd( f ) == f2@ ) {
-	// only handle IO failure for f2
-}
-\end{cfa}
-Here, matching is very precise on the I/O exception and particular file with an open problem.
-This capability cannot be easily mimiced within the handler.
 \begin{cfa}
 try {
@@ -497,22 +487,17 @@
 	f2 = open( ... );
 	...
-} catch( CreateFailure * f ) {
-	if ( @fd( f ) == f1@ ) ... else // reraise 
-} catch( OpenFailure * f ) {
-	if ( @fd( f ) == f2@ ) ... else // reraise 
+} catch( IOFailure * f ; fd( f ) == f1 ) {
+	// only handle IO failure for f1
 }
 \end{cfa}
-When an exception @CreateFailure@ is raised, the first handler catches the
-derived exception and reraises it if the object is inappropriate. The reraise
-immediately terminates the current guarded block, which precludes the handler
-for the base exception @OpenFailure@ from consideration for object
-@f2@. Therefore, the ``catch first, then reraise'' approach is an incomplete
-substitute for conditional catch.
-
-\section{Reraise}
+Note, catching @IOFailure@, checking for @f1@ in the handler, and re-raising the
+exception if not @f1@ is different because the re-raise does not examine any of
+remaining handlers in the current try statement.
+
+\section{Rethrowing}
+\colour{red}{From Andrew: I recomend we talk about why the language doesn't
+have rethrows/reraises instead.}
+
 \label{s:Rethrowing}
-\colour{red}{From Andrew: I recommend we talk about why the language doesn't
-have rethrows/reraises instead.}
-
 Within the handler block or functions called from the handler block, it is
 possible to reraise the most recently caught exception with @throw@ or
@@ -533,9 +518,8 @@
 is part of an unwound stack frame. To prevent this problem, a new default
 handler is generated that does a program-level abort.
-\PAB{I don't see how this is different from the normal throw/throwResume.}
 
 \section{Finally Clauses}
-Finally clauses are used to perform unconditional clean-up when leaving a
-scope and appear at the end of a try statement after any catch clauses:
+Finally clauses are used to preform unconditional clean-up when leaving a
+scope. They are placed at the end of a try statement:
 \begin{cfa}
 try {
@@ -548,30 +532,29 @@
 The @FINALLY_BLOCK@ is executed when the try statement is removed from the
 stack, including when the @GUARDED_BLOCK@ finishes, any termination handler
-finishes, or during an unwind.
+finishes or during an unwind.
 The only time the block is not executed is if the program is exited before
 the stack is unwound.
 
 Execution of the finally block should always finish, meaning control runs off
-the end of the block. This requirement ensures execution always continues as if the
-finally clause is not present, \ie @finally@ is for cleanup not changing control
+the end of the block. This requirement ensures always continues as if the
+finally clause is not present, \ie finally is for cleanup not changing control
 flow. Because of this requirement, local control flow out of the finally block
 is forbidden. The compiler precludes any @break@, @continue@, @fallthru@ or
 @return@ that causes control to leave the finally block. Other ways to leave
 the finally block, such as a long jump or termination are much harder to check,
-and at best require additional run-time overhead, and so are
+and at best requiring additional run-time overhead, and so are mealy
 discouraged.
 
 Not all languages with exceptions have finally clauses. Notably \Cpp does
-without it as destructors serve a similar role. Although destructors and
-finally clauses can be used in many of the same areas, they have their own
+without it as descructors serve a similar role. Although destructors and
+finally clauses can be used in many of the same areas they have their own
 use cases like top-level functions and lambda functions with closures.
 Destructors take a bit more work to set up but are much easier to reuse while
-finally clauses are good for one-off situations and can easily include local information.
+finally clauses are good for once offs and can include local information.
 
 \section{Cancellation}
-\label{s:Cancellation}
-Cancellation is a stack-level abort, which can be thought of as an
-uncatchable termination. It unwinds the entire stack, and when
-possible, forwards the cancellation exception to a different stack.
+Cancellation is a stack-level abort, which can be thought of as as an
+uncatchable termination. It unwinds the entirety of the current stack, and if
+possible forwards the cancellation exception to a different stack.
 
 Cancellation is not an exception operation like termination or resumption.
@@ -580,84 +563,34 @@
 throw, this exception is not used in matching only to pass information about
 the cause of the cancellation.
-(This semantics also means matching cannot fail so there is no default handler.)
-
-After @cancel_stack@ is called, the exception is copied into the EHM's
-memory and the current stack is
+(This also means matching cannot fail so there is no default handler either.)
+
+After @cancel_stack@ is called the exception is copied into the exception
+handling mechanism's memory. Then the entirety of the current stack is
 unwound. After that it depends one which stack is being cancelled.
 \begin{description}
 \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. Even in a concurrent program,
-the main stack is often used as the environment to start the concurrent threads.
+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 go. Hence, after the main stack is unwound, there is a program-level abort.
+to notify. After the stack is unwound, there is a program-level abort.
 
 \item[Thread Stack:]
-A thread stack is created for a \CFA @thread@ object or object that satisfies the
+A thread stack is created for a @thread@ object or object that satisfies the
 @is_thread@ trait. A thread only has two points of communication that must
-happen: start and join. A thread must be running to perform a
-cancellation (a thread cannot cancel another thread). Therefore, a cancellation must
-occur after start and before join, so join is used
-for cancellation communication.
+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 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@.
 
-\begin{sloppypar}
 There is a subtle difference between the explicit join (@join@ function) and
-implicit join (from a @thread@'s destructor call). The explicit join takes the default
+implicit join (from a destructor call). The explicit join takes the default
 handler (@defaultResumptionHandler@) from its calling context, which is used if
 the exception is not caught. The implicit join does a program abort instead.
-\end{sloppypar}
-
-\PAB{uC++ does not have these issues, but catch(...) is not working.}
-\begin{lstlisting}[language=uC++]
-#include <iostream>
-using namespace std;
-
-struct Cl {
-	~Cl() { cout << "C" << endl; }
-};
-_Coroutine C {
-	void main() {
-		Cl c;
-		try {
-			cancel();
-		} catch( ... ) {
-			cout << "..." << endl;
-		} _Finally {
-			cout << "F" << endl;
-		}
-		}
-  public:
-	void mem() { resume(); }
-};
-_Task T {
-	void main() {
-		Cl c;
-		try {
-			cancel();
-		} catch( ... ) {
-			cout << "..." << endl;
-		} _Finally {
-			cout << "F" << endl;
-		}
-	}
-};
-int main() {
-	C c;
-	cout << "here1" << endl;
-	c.mem();
-	cout << "here2" << endl;
-	{
-		T t;
-	}
-	cout << "here3" << endl;
-}
-\end{lstlisting}
-
-\PAB{This discussion should be its own section.}
+
 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
+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
@@ -665,5 +598,4 @@
 happen in an implicate join inside a destructor. So there is an error message
 and an abort instead.
-
 \todo{Perhaps have a more general disucssion of unwind collisions before
 this point.}
@@ -688,4 +620,2 @@
 for the exception. So it will use the default handler like a regular throw.
 \end{description}
-
-\PAB{You should have more test programs that compare \CFA EHM to uC++ EHM.}
Index: doc/theses/andrew_beach_MMath/stackMarking.fig
===================================================================
--- doc/theses/andrew_beach_MMath/stackMarking.fig	(revision 47e000c054a8dc58293a93fbc643e10735fd30f9)
+++ 	(revision )
@@ -1,40 +1,0 @@
-#FIG 3.2  Produced by xfig version 3.2.7b
-Landscape
-Center
-Inches
-Letter
-100.00
-Single
--2
-1200 2
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
-	 1800 1275 1800 1425
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 3
-	1 1 1.00 45.00 90.00
-	 2625 1125 3225 1125 3225 2400
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
-	 1800 1725 1800 1875
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
-	 1800 2175 1800 2325
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
-	 1800 2625 1800 2775
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
-	 1800 3000 1800 3150
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
-	 1800 3375 1800 3525
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 4
-	1 1 1.00 45.00 90.00
-	 2625 2475 2850 2475 2850 3225 2625 3225
-2 1 1 1 0 7 50 -1 -1 4.000 0 0 -1 0 0 2
-	 3225 2475 3225 3225
-2 1 0 1 0 7 50 -1 -1 4.000 0 0 -1 1 0 2
-	1 1 1.00 45.00 90.00
-	 3225 3300 3225 3525
-4 1 0 50 -1 5 12 0.0000 2 120 1440 1800 1200 throwResume2\001
-4 1 0 50 -1 5 12 0.0000 2 165 2640 1800 1650 generated from handler\001
-4 1 0 50 -1 5 12 0.0000 2 120 840 1800 2100 handler\001
-4 1 0 50 -1 5 12 0.0000 2 120 1440 1875 2550 throwResume1\001
-4 1 0 50 -1 5 12 0.0000 2 150 360 1800 2925 try\001
-4 1 0 50 -1 5 12 0.0000 2 120 1320 1800 3300 catchresume\001
-4 2 0 50 -1 0 12 0.0000 2 135 600 2775 2925 marked\001
-4 0 0 50 -1 0 12 0.0000 2 180 900 3375 2925 search skip\001
Index: doc/theses/andrew_beach_MMath/uw-ethesis.tex
===================================================================
--- doc/theses/andrew_beach_MMath/uw-ethesis.tex	(revision 47e000c054a8dc58293a93fbc643e10735fd30f9)
+++ doc/theses/andrew_beach_MMath/uw-ethesis.tex	(revision de47a9d90448b4a9998ca306ff8576f8cd4f3369)
@@ -105,7 +105,5 @@
 \usepackage{amsmath,amssymb,amstext}
 % For including graphics N.B. pdftex graphics driver
-%\usepackage[pdftex]{graphicx}
-\usepackage{epic,eepic}
-\usepackage{graphicx}
+\usepackage[pdftex]{graphicx}
 % Removes large sections of the document.
 \usepackage{comment}
@@ -119,6 +117,5 @@
 % Use the "hyperref" package
 % N.B. HYPERREF MUST BE THE LAST PACKAGE LOADED; ADD ADDITIONAL PKGS ABOVE
-%\usepackage[pdftex,pagebackref=true]{hyperref} % with basic options
-\usepackage[pagebackref=true]{hyperref} % with basic options
+\usepackage[pdftex,pagebackref=true]{hyperref} % with basic options
 %\usepackage[pdftex,pagebackref=true]{hyperref}
 % N.B. pagebackref=true provides links back from the References to the body
