Index: doc/theses/andrew_beach_MMath/features.tex
===================================================================
--- doc/theses/andrew_beach_MMath/features.tex	(revision 471ff179f9b2e7085350b2cdde0c50124be88f60)
+++ doc/theses/andrew_beach_MMath/features.tex	(revision 4aba055ca036651cf2078e21d8d23aa2d7b78fc2)
@@ -2,24 +2,23 @@
 \label{c:features}
 
-This chapter covers the design and user interface of the \CFA
-exception-handling mechanism (EHM). % or exception system.
-
-We will begin with an overview of EHMs in general. It is not a strict
-definition of all EHMs nor an exaustive list of all possible features.
+This chapter covers the design and user interface of the \CFA EHM
+and begins with a general overview of EHMs. It is not a strict
+definition of all EHMs nor an exhaustive list of all possible features.
 However it does cover the most common structure and features found in them.
 
+\section{Overview of EHMs}
 % We should cover what is an exception handling mechanism and what is an
 % exception before this. Probably in the introduction. Some of this could
 % move there.
-\paragraph{Raise / Handle}
+\subsection{Raise / Handle}
 An exception operation has two main parts: raise and handle.
 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 that the user will write themselves and may
+These are the two parts that the user writes and may
 be the only two pieces of the EHM that have any syntax in the language.
 
-\subparagraph{Raise}
+\paragraph{Raise}
 The raise is the starting point for exception handling. It marks the beginning
-of exception handling by raising an excepion, which passes it to
+of exception handling by raising an exception, which passes it to
 the EHM.
 
@@ -29,44 +28,44 @@
 purposes of this overview that can be ignored.
 
-\subparagraph{Handle}
+\paragraph{Handle}
 The purpose of most exception operations is to run some user code to handle
 that exception. This code is given, with some other information, in a handler.
 
 A handler has three common features: the previously mentioned user code, a
-region of code they cover and an exception label/condition that matches
+region of code they guard and an exception label/condition that matches
 certain exceptions.
-Only raises inside the covered region and raising exceptions that match the
+Only raises inside the guarded region and raising exceptions that match the
 label can be handled by a given handler.
-Different EHMs will have different rules to pick a handler
-if multipe handlers could be used such as ``best match" or ``first found".
+Different EHMs use different rules to pick a handler,
+if multiple handlers could be used such as ``best match" or ``first found".
 
 The @try@ statements of \Cpp, Java and Python are common examples. All three
-also show another common feature of handlers, they are grouped by the covered
+also show another common feature of handlers, they are grouped by the guarded
 region.
 
-\paragraph{Propagation}
+\subsection{Propagation}
 After an exception is raised comes what is usually the biggest step for the
-EHM: finding and setting up the handler. The propogation from raise to
+EHM: finding and setting up the handler. The propagation from raise to
 handler can be broken up into three different tasks: searching for a handler,
 matching against the handler and installing the handler.
 
-\subparagraph{Searching}
+\paragraph{Searching}
 The EHM begins by searching for handlers that might be used to handle
 the exception. Searching is usually independent of the exception that was
-thrown as it looks for handlers that have the raise site in their covered
+thrown as it looks for handlers that have the raise site in their guarded
 region.
-This includes handlers in the current function, as well as any in callers
-on the stack that have the function call in their covered region.
-
-\subparagraph{Matching}
+The search includes handlers in the current function, as well as any in
+callers on the stack that have the function call in their guarded region.
+
+\paragraph{Matching}
 Each handler found has to be matched with the raised exception. The exception
-label defines a condition that be use used with exception and decides if
+label defines a condition that is used with exception and decides if
 there is a match or not.
 
-In languages where the first match is used this step is intertwined with
-searching, a match check is preformed immediately after the search finds
+In languages where the first match is used, this step is intertwined with
+searching; a match check is preformed immediately after the search finds
 a possible handler.
 
-\subparagraph{Installing}
+\paragraph{Installing}
 After a handler is chosen it must be made ready to run.
 The implementation can vary widely to fit with the rest of the
@@ -75,14 +74,13 @@
 case when stack unwinding is involved.
 
-If a matching handler is not guarantied to be found the EHM will need a
-different course of action here in the cases where no handler matches.
-This is only required with unchecked exceptions as checked exceptions
-(such as in Java) can make than guaranty.
-This different action can also be installing a handler but it is usually an
-implicat and much more general one.
-
-\subparagraph{Hierarchy}
+If a matching handler is not guarantied to be found, the EHM needs a
+different course of action for the case where no handler matches.
+This situation only occurs with unchecked exceptions as checked exceptions
+(such as in Java) can make the guarantee.
+This unhandled action is usually very general, such as aborting the program.
+
+\paragraph{Hierarchy}
 A common way to organize exceptions is in a hierarchical structure.
-This is especially true in object-orientated languages where the
+This pattern comes from object-orientated languages where the
 exception hierarchy is a natural extension of the object hierarchy.
 
@@ -92,5 +90,5 @@
 \end{center}
 
-A handler labelled with any given exception can handle exceptions of that
+A handler labeled with any given exception can handle exceptions of that
 type or any child type of that exception. The root of the exception hierarchy
 (here \code{C}{exception}) acts as a catch-all, leaf types catch single types
@@ -106,5 +104,5 @@
 % Could I cite the rational for the Python IO exception rework?
 
-\paragraph{Completion}
+\subsection{Completion}
 After the handler has finished the entire exception operation has to complete
 and continue executing somewhere else. This step is usually simple,
@@ -113,27 +111,30 @@
 
 The EHM can return control to many different places,
-the most common are after the handler definition and after the raise.
-
-\paragraph{Communication}
+the most common are after the handler definition (termination)
+and after the raise (resumption).
+
+\subsection{Communication}
 For effective exception handling, additional information is often passed
-from the raise to the handler.
+from the raise to the handler and back again.
 So far only communication of the exceptions' identity has been covered.
-A common method is putting fields into the exception instance and giving the
-handler access to them.
+A common communication method is putting fields into the exception instance
+and giving the handler access to them.
+Passing the exception by reference instead of by value can allow data to be
+passed in both directions.
 
 \section{Virtuals}
 Virtual types and casts are not part of \CFA's EHM nor are they required for
 any EHM.
-However the \CFA uses a hierarchy built with the virtual system as the basis
-for exceptions and exception matching.
-
-The virtual system would have ideally been part of \CFA before the work
+However, it is one of the best ways to support an exception hierachy
+is via a virtual hierarchy and dispatch system.
+
+Ideally, the virtual system would have been part of \CFA before the work
 on exception handling began, but unfortunately it was not.
-Because of this only the features and framework needed for the EHM were
+Hence, only the features and framework needed for the EHM were
 designed and implemented. Other features were considered to ensure that
-the structure could accomidate other desirable features but they were not
-implemented.
-The rest of this section will only discuss the finalized portion of the
-virtual system.
+the structure could accommodate other desirable features in the future
+but they were not implemented.
+The rest of this section will only discuss the implemented subset of the
+virtual system design.
 
 The virtual system supports multiple ``trees" of types. Each tree is
@@ -145,5 +146,5 @@
 % A type's ancestors are its parent and its parent's ancestors.
 % The root type has no ancestors.
-% A type's decendents are its children and its children's decendents.
+% A type's descendants are its children and its children's descendants.
 
 Every virtual type also has a list of virtual members. Children inherit
@@ -151,34 +152,37 @@
 It is important to note that these are virtual members, not virtual methods
 of object-orientated programming, and can be of any type.
+
 \CFA still supports virtual methods as a special case of virtual members.
-Function pointers that take a pointer to the virtual type will be modified
+Function pointers that take a pointer to the virtual type are modified
 with each level of inheritance so that refers to the new type.
 This means an object can always be passed to a function in its virtual table
 as if it were a method.
+\todo{Clarify (with an example) virtual methods.}
 
 Each virtual type has a unique id.
-This unique id and all the virtual members are combined
+This id 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.
+\todo{Might need a diagram for virtual structure.}
 
 Up until this point the virtual system is similar to ones found in
 object-orientated languages but this where \CFA diverges. 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.
 
-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
+In \CFA, types do not encapsulate any behaviour. Traits are local and
+types can begin to satisfy a trait, stop satisfying a trait or satisfy the same
 trait in a different way at any lexical location in the program.
-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's
-implementation across the program.
+In this sense, they are ``open" as they can change at any time.
+This capability means it is impossible to pick a single set of functions
+that represent the type's implementation across the program.
 
 \CFA side-steps this issue by not having a single virtual table for each
-type. A user can define virtual tables which are filled in at their
-declaration and given a name. Anywhere that name is visible, even if it was
-defined locally inside a function (although that means it will not have a
+type. A user can define virtual tables that are filled in at their
+declaration and given a name. Anywhere that name is visible, even if it is
+defined locally inside a function (although that means it does not have a
 static lifetime), it can be used.
-Specifically, a virtual type is ``bound" to a virtual table which
+Specifically, a virtual type is ``bound" to a virtual table that
 sets the virtual members for that object. The virtual members can be accessed
 through the object.
@@ -212,10 +216,10 @@
 \end{cfa}
 The trait is defined over two types, the exception type and the virtual table
-type. Each exception type should have but a single virtual table type.
-Now there are no actual assertions in this trait because the trait system
-actually can't express them (adding such assertions would be part of
+type. Each exception type should have a single virtual table type.
+There are no actual assertions in this trait because the trait system
+cannot express them yet (adding such assertions would be part of
 completing the virtual system). The imaginary assertions would probably come
 from a trait defined by the virtual system, and state that the exception type
-is a virtual type, is a decendent of @exception_t@ (the base exception type)
+is a virtual type, is a descendant of @exception_t@ (the base exception type)
 and note its virtual table type.
 
@@ -236,5 +240,6 @@
 };
 \end{cfa}
-Both traits ensure a pair of types are an exception type and its virtual table
+Both traits ensure a pair of types are an exception type, its virtual table
+type
 and defines one of the two default handlers. The default handlers are used
 as fallbacks and are discussed in detail in \vref{s:ExceptionHandling}.
@@ -264,4 +269,5 @@
 \section{Exception Handling}
 \label{s:ExceptionHandling}
+As stated,
 \CFA provides two kinds of exception handling: termination and resumption.
 These twin operations are the core of \CFA's exception handling mechanism.
@@ -271,12 +277,12 @@
 Both operations follow the same set of steps.
 Both start with the user preforming a raise on an exception.
-Then the exception propogates up the stack.
+Then the exception propagates up the stack.
 If a handler is found 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 after the raise.
+After that control continues at a raise-dependent location.
+If the search fails a default handler is run and, if it returns, then control
+continues after the raise.
 
 This general description covers what the two kinds have in common.
-Differences include how propogation is preformed, where exception continues
+Differences include how propagation is preformed, where exception continues
 after an exception is caught and handled and which default handler is run.
 
@@ -285,6 +291,6 @@
 Termination handling is the familiar kind and used in most programming
 languages with exception handling.
-It is dynamic, non-local goto. If the raised exception is matched and
-handled the stack is unwound and control will (usually) continue the function
+It is a dynamic, non-local goto. If the raised exception is matched and
+handled, the stack is unwound and control (usually) continues in the function
 on the call stack that defined the handler.
 Termination is commonly used when an error has occurred and recovery is
@@ -301,18 +307,19 @@
 termination exception is any type that satisfies the trait
 @is_termination_exception@ at the call site.
-Through \CFA's trait system the trait functions are implicity passed into the
+Through \CFA's trait system, the trait functions are implicitly passed into the
 throw code and the EHM.
 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 to ensure
+change the throw's behaviour (see below).
+
+The throw copies the provided exception into managed memory to ensure
 the exception is not destroyed if the stack is unwound.
 It is the user's responsibility to ensure the original exception is cleaned
-up wheither the stack is unwound or not. Allocating it on the stack is
+up whether the stack is unwound or not. Allocating it on the stack is
 usually sufficient.
 
-Then propogation starts with the search. \CFA uses a ``first match" rule so
+% How to say propagation starts, its first sub-step is the search.
+Then propagation starts with the search. \CFA uses a ``first match" rule so
 matching is preformed with the copied exception as the search continues.
-It starts from the throwing function and proceeds to the base of the stack,
+It starts from the throwing function and proceeds towards base of the stack,
 from callee to caller.
 At each stack frame, a check is made for resumption handlers defined by the
@@ -327,14 +334,16 @@
 }
 \end{cfa}
-When viewed on its own, a try statement will simply execute the statements
-in \snake{GUARDED_BLOCK} and when those are finished the try statement finishes.
+When viewed on its own, a try statement simply executes the statements
+in \snake{GUARDED_BLOCK} and when those are finished,
+the try statement finishes.
 
 However, while the guarded statements are being executed, including any
-invoked functions, all the handlers in the statement are now on the search
-path. If a termination exception is thrown and not handled further up the
-stack they will be matched against the exception.
+invoked functions, all the handlers in these statements are included in the
+search path.
+Hence, if a termination exception is raised these handlers may be matched
+against the exception and may handle it.
 
 Exception matching checks the handler in each catch clause in the order
-they appear, top to bottom. If the representation of the thrown exception type
+they appear, top to bottom. If the representation of the raised exception type
 is the same or a descendant of @EXCEPTION_TYPE@$_i$ then @NAME@$_i$
 (if provided) is
@@ -344,13 +353,14 @@
 
 If no termination handler is found during the search then the default handler
-(\defaultTerminationHandler) 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.
+(\defaultTerminationHandler) visible at the raise statement is run.
+Through \CFA's trait system the best match at the raise statement will be used.
+This function is run and is passed the copied exception.
+If the default handler is run control continues after the raise statement.
 
 There is a global @defaultTerminationHandler@ that is polymorphic over all
-exception types. Since it is so general a more specific handler can be
-defined and will be used for those types, effectively overriding the handler
-for particular exception type.
+termination exception types.
+Since it is so general a more specific handler can be
+defined and is used for those types, effectively overriding the handler
+for a particular exception type.
 The global default termination handler performs a cancellation
 (see \vref{s:Cancellation}) on the current stack with the copied exception.
@@ -362,8 +372,11 @@
 just as old~\cite{Goodenough75} and is simpler in many ways.
 It is a dynamic, non-local function call. If the raised exception is
-matched a closure will be taken from up the stack and executed,
-after which the raising function will continue executing.
-These are most often used when an error occurred and if the error is repaired
-then the function can continue.
+matched a closure is taken from up the stack and executed,
+after which the raising function continues executing.
+The common uses for resumption exceptions include
+potentially repairable errors, where execution can continue in the same
+function once the error is corrected, and
+ignorable events, such as logging where nothing needs to happen and control
+should always continue from the same place.
 
 A resumption raise is started with the @throwResume@ statement:
@@ -371,4 +384,5 @@
 throwResume EXPRESSION;
 \end{cfa}
+\todo{Decide on a final set of keywords and use them everywhere.}
 It works much the same way as the termination throw.
 The expression must return a reference to a resumption exception,
@@ -379,9 +393,10 @@
 
 At run-time, no exception copy is made.
-As the stack is not unwound the exception and
-any values on the stack will remain in scope while the resumption is handled.
-
-The EHM then begins propogation. The search starts from the raise in the
-resuming function and proceeds to the base of the stack, from callee to caller.
+Resumption does not unwind the stack nor otherwise remove values from the
+current scope, so there is no need to manage memory to keep things in scope.
+
+The EHM then begins propagation. The search starts from the raise in the
+resuming function and proceeds towards 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.
@@ -398,16 +413,17 @@
 Note that termination handlers and resumption handlers may be used together
 in a single try statement, intermixing @catch@ and @catchResume@ freely.
-Each type of handler will only interact with exceptions from the matching
-type of raise.
-When a try statement is executed it simply executes the statements in the
+Each type of handler only interacts with exceptions from the matching
+kind of raise.
+When a try statement is executed, it simply executes the statements in the
 @GUARDED_BLOCK@ and then finishes.
 
 However, while the guarded statements are being executed, including any
-invoked functions, all the handlers in the statement are now on the search
-path. If a resumption exception is reported and not handled further up the
-stack they will be matched against the exception.
+invoked functions, all the handlers in these statements are included in the
+search path.
+Hence, if a resumption exception is raised these handlers may be matched
+against the exception and may handle it.
 
 Exception matching checks the handler in each catch clause in the order
-they appear, top to bottom. If the representation of the thrown exception type
+they appear, top to bottom. If the representation of the raised exception type
 is the same or a descendant of @EXCEPTION_TYPE@$_i$ then @NAME@$_i$
 (if provided) is bound to a pointer to the exception and the statements in
@@ -416,15 +432,15 @@
 the raise statement that raised the handled exception.
 
-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
+Like termination, if no resumption handler is found during the search,
+the default handler (\defaultResumptionHandler) visible at the raise
+statement is called. It will use the best match at the raise sight according
+to \CFA's overloading rules. The default handler is
+passed the exception given to the raise. When the default handler finishes
 execution continues after the raise statement.
 
 There is a global \defaultResumptionHandler{} is polymorphic over all
-termination exceptions and preforms a termination throw on the exception.
-The \defaultTerminationHandler{} for that raise is matched at the
-original raise statement (the resumption @throw@\-@Resume@) and it can be
-customized by introducing a new or better match as well.
+resumption exceptions and preforms a termination throw on the exception.
+The \defaultTerminationHandler{} can be overriden by providing a new
+function that is a better match.
 
 \subsubsection{Resumption Marking}
@@ -433,6 +449,6 @@
 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.
+searched before it are still on the stack. There presence can lead to
+the recursive resumption problem.
 
 The recursive resumption problem is any situation where a resumption handler
@@ -446,18 +462,18 @@
 }
 \end{cfa}
-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.
-
-This situation is trivial and easy to avoid, but much more complex cycles
+When this code is executed, the guarded @throwResume@ starts a
+search and matches the handler in the @catchResume@ clause. This
+call is placed on the stack above the try-block. The second raise then
+searches the same try block and puts another instance of the
+same handler on the stack leading to infinite recursion.
+
+While this situation is trivial and easy to avoid, much more complex cycles
 can form with multiple handlers and different exception types.
 
-To prevent all of these cases we mark try statements on the stack.
-A try statement is marked when a match check is preformed with it and an
-exception. The statement will be unmarked when the handling of that exception
-is completed or the search completes without finding a handler.
-While a try statement is marked its handlers are never matched, effectify
+To prevent all of these cases, a each try statement is ``marked" from the
+time the exception search reaches it to either when the exception is being
+handled completes the matching handler or when the search reaches the base
+of the stack.
+While a try statement is marked, its handlers are never matched, effectively
 skipping over it to the next try statement.
 
@@ -466,15 +482,17 @@
 \end{center}
 
-These rules mirror what happens with termination.
-When a termination throw happens in a handler the search will not look at
-any handlers from the original throw to the original catch because that
-part of the stack has been unwound.
-A resumption raise in the same situation wants to search the entire stack,
-but it will not try to match the exception with try statements in the section
-that would have been unwound as they are marked.
-
-The symmetry between resumption termination is why this pattern was picked.
-Other patterns, such as marking just the handlers that caught, also work but
-lack the symmetry means there are more rules to remember.
+There are other sets of marking rules that could be used,
+for instance, marking just the handlers that caught the exception,
+would also prevent recursive resumption.
+However, these rules mirror what happens with termination.
+
+The try statements that are marked are the ones that would be removed from
+the stack if this was a termination exception, that is those on the stack
+between the handler and the raise statement.
+This symmetry applies to the default handler as well, as both kinds of
+default handlers are run at the raise statement, rather than (physically
+or logically) at the bottom of the stack.
+% In early development having the default handler happen after
+% unmarking was just more useful. We assume that will continue.
 
 \section{Conditional Catch}
@@ -491,5 +509,5 @@
 did not match.
 
-The condition matching allows finer matching by allowing the match to check
+The condition matching allows finer matching by checking
 more kinds of information than just the exception type.
 \begin{cfa}
@@ -506,5 +524,5 @@
 // Can't handle a failure relating to f2 here.
 \end{cfa}
-In this example the file that experianced the IO error is used to decide
+In this example the file that experienced the IO error is used to decide
 which handler should be run, if any at all.
 
@@ -536,9 +554,10 @@
 \subsection{Comparison with Reraising}
 A more popular way to allow handlers to match in more detail is to reraise
-the exception after it has been caught if it could not be handled here.
-On the surface these two features seem interchangable.
-
-If we used @throw;@ to start a termination reraise then these two statements
-would have the same behaviour:
+the exception after it has been caught, if it could not be handled here.
+On the surface these two features seem interchangeable.
+
+If @throw;@ (no argument) starts a termination reraise,
+which is the same as a raise but reuses the last caught exception,
+then these two statements have the same behaviour:
 \begin{cfa}
 try {
@@ -560,27 +579,62 @@
 }
 \end{cfa}
-If there are further handlers after this handler only the first version will
-check them. If multiple handlers on a single try block that could handle the
-same exception the translations get more complex but they are equivilantly
-powerful.
-
-Until stack unwinding comes into the picture. In termination handling, a
-conditional catch happens before the stack is unwound, but a reraise happens
-afterwards. Normally this might only cause you to loose some debug
-information you could get from a stack trace (and that can be side stepped
-entirely by collecting information during the unwind). But for \CFA there is
-another issue, if the exception isn't handled the default handler should be
-run at the site of the original raise.
-
-There are two problems with this: the site of the original raise doesn't
-exist anymore and the default handler might not exist anymore. The site will
-always be removed as part of the unwinding, often with the entirety of the
-function it was in. The default handler could be a stack allocated nested
-function removed during the unwind.
-
-This means actually trying to pretend the catch didn't happening, continuing
-the original raise instead of starting a new one, is infeasible.
-That is the expected behaviour for most languages and we can't replicate
-that behaviour.
+That is, they will have the same behaviour in isolation.
+Two things can expose differences between these cases.
+
+One is the existance of multiple handlers on a single try statement.
+A reraise skips all later handlers on this try statement but a conditional
+catch does not.
+Hence, if an earlier handler contains a reraise later handlers are
+implicitly skipped, with a conditional catch they are not.
+Still, they are equivalently powerful,
+both can be used two mimick the behaviour of the other,
+as reraise can pack arbitrary code in the handler and conditional catches
+can put arbitrary code in the predicate.
+% I was struggling with a long explination about some simple solutions,
+% like repeating a condition on later handlers, and the general solution of
+% merging everything together. I don't think it is useful though unless its
+% for a proof.
+% https://en.cppreference.com/w/cpp/language/throw
+
+The question then becomes ``Which is a better default?"
+We believe that not skipping possibly useful handlers is a better default.
+If a handler can handle an exception it should and if the handler can not
+handle the exception then it is probably safer to have that explicitly
+described in the handler itself instead of implicitly described by its
+ordering with other handlers.
+% Or you could just alter the semantics of the throw statement. The handler
+% index is in the exception so you could use it to know where to start
+% searching from in the current try statement.
+% No place for the `goto else;` metaphor.
+
+The other issue is all of the discussion above assumes that the only
+way to tell apart two raises is the exception being raised and the remaining
+search path.
+This is not true generally, the current state of the stack can matter in
+a number of cases, even only for a stack trace after an program abort.
+But \CFA has a much more significant need of the rest of the stack, the
+default handlers for both termination and resumption.
+
+% For resumption it turns out it is possible continue a raise after the
+% exception has been caught, as if it hadn't been caught in the first place.
+This becomes a problem combined with the stack unwinding used in termination
+exception handling.
+The stack is unwound before the handler is installed, and hence before any
+reraises can run. So if a reraise happens the previous stack is gone,
+the place on the stack where the default handler was supposed to run is gone,
+if the default handler was a local function it may have been unwound too.
+There is no reasonable way to restore that information, so the reraise has
+to be considered as a new raise.
+This is the strongest advantage conditional catches have over reraising,
+they happen before stack unwinding and avoid this problem.
+
+% The one possible disadvantage of conditional catch is that it runs user
+% code during the exception search. While this is a new place that user code
+% can be run destructors and finally clauses are already run during the stack
+% unwinding.
+%
+% https://www.cplusplus.com/reference/exception/current_exception/
+%   `exception_ptr current_exception() noexcept;`
+% https://www.python.org/dev/peps/pep-0343/
 
 \section{Finally Clauses}
@@ -614,10 +668,15 @@
 
 Not all languages with unwinding have finally clauses. Notably \Cpp does
-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 uses and
-can easily include local information.
+without it as descructors, and the RAII design pattern, serve a similar role.
+Although destructors and finally clauses can be used in the same cases,
+they have their own strengths, similar to top-level function and lambda
+functions with closures.
+Destructors take more work for their first use, but if there is clean-up code
+that needs to be run every time a type is used they soon become much easier
+to set-up.
+On the other hand finally clauses capture the local context, so is easy to
+use when the clean-up is not dependent on the type of a variable or requires
+information from multiple variables.
+% To Peter: I think these are the main points you were going for.
 
 \section{Cancellation}
@@ -635,6 +694,6 @@
 
 After @cancel_stack@ is called the exception is copied into the EHM's memory
-and the current stack is
-unwound. After that it depends one which stack is being cancelled.
+and the current stack is unwound.
+The behaviour after that depends on the kind of stack being cancelled.
 
 \paragraph{Main Stack}
@@ -643,28 +702,30 @@
 After the main stack is unwound there is a program-level abort. 
 
-There are two reasons for this. The first is that it obviously had to do this
+There are two reasons for these semantics.
+The first is that it had to do this abort.
 in a sequential program as there is nothing else to notify and the simplicity
 of keeping the same behaviour in sequential and concurrent programs is good.
-Also, even in concurrent programs there is no stack that an innate connection
-to, so it would have be explicitly managed.
+Also, even in concurrent programs there may not currently be any other stacks
+and even if other stacks do exist, main has no way to know where they are.
 
 \paragraph{Thread Stack}
 A thread stack is created for a \CFA @thread@ object or object that satisfies
 the @is_thread@ trait.
-After a thread stack is unwound there exception is stored until another
+After a thread stack is unwound, the exception is stored until another
 thread attempts to join with it. Then the exception @ThreadCancelled@,
 which stores a reference to the thread and to the exception passed to the
-cancellation, is reported from the join.
+cancellation, is reported from the join to the joining thread.
 There is one difference between an explicit join (with the @join@ function)
 and an implicit join (from a destructor call). The explicit join takes the
 default handler (@defaultResumptionHandler@) from its calling context while
-the implicit join provides its own which does a program abort if the
+the implicit join provides its own; which does a program abort if the
 @ThreadCancelled@ exception cannot be handled.
 
-Communication is done at join because a thread only has to have to points of
-communication with other threads: start and join.
+The communication and synchronization are done here because threads only have
+two structural points (not dependent on user-code) where
+communication/synchronization happens: start and join.
 Since a thread must be running to perform a cancellation (and cannot be
 cancelled from another stack), the cancellation must be after start and
-before the join. So join is the one that we will use.
+before the join, so join is used.
 
 % TODO: Find somewhere to discuss unwind collisions.
@@ -678,13 +739,13 @@
 A coroutine stack is created for a @coroutine@ object or object that
 satisfies the @is_coroutine@ trait.
-After a coroutine stack is unwound control returns to the resume function
-that most recently resumed it. The resume statement reports a
+After a coroutine stack is unwound, control returns to the @resume@ function
+that most recently resumed it. @resume@ reports a
 @CoroutineCancelled@ exception, which contains a references to the cancelled
 coroutine and the exception used to cancel it.
-The resume function also takes the \defaultResumptionHandler{} from the
+The @resume@ function also takes the \defaultResumptionHandler{} from the
 caller's context and passes it to the internal report.
 
 A coroutine knows of two other coroutines, its starter and its last resumer.
-The starter has a much more distant connection while the last resumer just
+The starter has a much more distant connection, while the last resumer just
 (in terms of coroutine state) called resume on this coroutine, so the message
 is passed to the latter.
