--- a/ProgTutorial/Advanced.thy	Mon Nov 07 10:49:25 2011 +0000
+++ b/ProgTutorial/Advanced.thy	Mon Nov 07 13:36:07 2011 +0000
@@ -35,11 +35,12 @@
 section {* Theories and Setups\label{sec:theories} *}
 
 text {*
-  Theories, as said above, are a basic layer of abstraction in Isabelle. They
-  contain definitions, syntax declarations, axioms, theorems and much more. If a
-  definition is made, it must be stored in a theory in order to be usable
-  later on. Similar with proofs: once a proof is finished, the proved theorem
-  needs to be stored in the theorem database of the theory in order to be
+  Theories, as said above, are a basic layer of abstraction in
+  Isabelle. They contain definitions, syntax declarations, axioms,
+  theorems and much more.  For example, if a definition is made, it
+  must be stored in a theory in order to be usable later on. Similar
+  with proofs: once a proof is finished, the proved theorem needs to
+  be stored in the theorem database of the theory in order to be
   usable. All relevant data of a theory can be queried as follows.
 
   \begin{isabelle}
@@ -62,12 +63,12 @@
   for example the function @{ML read_term_global in Syntax} in the structure
   @{ML_struct Syntax}. The reason is to set them syntactically apart from
   functions acting on contexts or local theories (which will be discussed in
-  next sections). There is a tendency in the Isabelle development to prefer
+  the next sections). There is a tendency in the Isabelle development to prefer
   ``non-global'' operations, because they have some advantages, as we will also
   discuss later. However, some basic management of theories will very likely
   never go away.
 
-  In the context ML-programming, the most important command with theories
+  In the context of ML-programming, the most important command with theories
   is \isacommand{setup}. In the previous chapters we used it, for
   example, to make a theorem attribute known to Isabelle or to register a theorem
   under a name. What happens behind the scenes is that \isacommand{setup}
@@ -88,10 +89,10 @@
 end*}
 
 text {*
-  If you simply write this code\footnote{Recall that ML-code needs to be enclosed in
+  If you simply run this code\footnote{Recall that ML-code needs to be enclosed in
   \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} with the
-  intention of declaring a constant @{text "BAR"} with type @{typ nat} and run
-  the code, then indeed you obtain a theory as result. But if you query the
+  intention of declaring a constant @{text "BAR"} with type @{typ nat}, then 
+  indeed you obtain a theory as result. But if you query the
   constant on the Isabelle level using the command \isacommand{term}
 
   \begin{isabelle}
@@ -145,8 +146,8 @@
   \end{isabelle}
 
   This time we erroneously return the original theory @{text thy}, instead of
-  the modified one @{text thy'}. Such programming errors with handling the
-  most current theory will always result into stale theory error messages.
+  the modified one @{text thy'}. Such buggy code will always result into 
+  a runtime error message about stale theories.
 
   However, sometimes it does make sense to work with two theories at the same
   time, especially in the context of parsing and typing. In the code below we
@@ -175,7 +176,7 @@
   times the string is @{text [quotes] "FOO baz"}). But since we parse the string
   once in the context of the theory @{text tmp_thy'} in which @{text FOO} is
   declared to be a constant of type @{typ "nat \<Rightarrow>nat"} and once in the context 
-  of @{text thy}, we obtain two different terms, namely 
+  of @{text thy} where it is not, we obtain two different terms, namely 
 
   \begin{isabelle}
   \begin{graybox}
@@ -185,10 +186,10 @@
   \end{isabelle}
 
   There are two reasons for parsing a term in a temporary theory. One is to
-  obtain fully qualified names and the other is appropriate type inference.
-  This is relevant in situations where definitions are made later, but parsing
-  and type inference has to take already proceed as if the definitions were
-  already made.
+  obtain fully qualified names for constants and the other is appropriate type 
+  inference. This is relevant in situations where definitions are made later, 
+  but parsing and type inference has to take already proceed as if the definitions 
+  were already made.
 *}
 
 section {* Contexts (TBD) *}
@@ -198,8 +199,22 @@
   contain ``short-term memory data''. The reason is that a vast number of
   functions in Isabelle depend one way or the other on contexts. Even such
   mundane operation like printing out a term make essential use of contexts.
+  For this consider the following contrived proof which only purpose is to 
+  fix two variables 
 *}
 
+lemma "True"
+proof -
+  txt_raw {*\mbox{}\\[-6mm]*} 
+  ML_prf {* Variable.dest_fixes @{context} *} 
+  txt_raw {*\mbox{}\\[-6mm]*}
+  fix x y  
+  txt_raw {*\mbox{}\\[-6mm]*}
+  ML_prf {* Variable.dest_fixes @{context} *} 
+  txt_raw {*\mbox{}\\[-6mm]*}
+oops
+
+
 (*
 ML{*Proof_Context.debug := true*}
 ML{*Proof_Context.verbose := true*}

--- a/ProgTutorial/Base.thy	Mon Nov 07 10:49:25 2011 +0000
+++ b/ProgTutorial/Base.thy	Mon Nov 07 13:36:07 2011 +0000
@@ -101,10 +101,11 @@
            (fn () => ML_Context.eval_text true pos txt) 
               #> propagate_env #> Context.map_theory (write_file_ml_blk txt))))
 *}
+
 ML {*
 val _ =
   Outer_Syntax.command "ML_prf" "ML text within proof" 
-    (Keyword.tag "TutorialML" Keyword.prf_decl)
+    (Keyword.tag "TutorialMLprf" Keyword.prf_decl)
     (Parse.ML_source >> (fn (txt, pos) =>
       Toplevel.proof (Proof.map_context (Context.proof_map
         (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> propagate_env_prf)))

--- a/ProgTutorial/document/root.tex	Mon Nov 07 10:49:25 2011 +0000
+++ b/ProgTutorial/document/root.tex	Mon Nov 07 13:36:07 2011 +0000
@@ -88,6 +88,9 @@
 \newenvironment{graybox}
 {\def\FrameCommand{\fboxsep=1pt\colorbox{gray!20}}\MakeFramed{\smallskip\FrameRestore}}
 {\smallskip\endMakeFramed}
+\newenvironment{grayboxwithoutsep}
+{\def\FrameCommand{\fboxsep=1pt\colorbox{gray!20}}\MakeFramed{\FrameRestore}}
+{\endMakeFramed}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % this hack is for getting rid of the ML {* ... *} 
@@ -101,6 +104,10 @@
 \renewcommand{\isatagTutorialML}{\begin{vanishML}\begin{graybox}}
 \renewcommand{\endisatagTutorialML}{\end{graybox}\end{vanishML}}
 
+\isakeeptag{TutorialMLprf}
+\renewcommand{\isatagTutorialMLprf}{\begin{grayboxwithoutsep}}
+\renewcommand{\endisatagTutorialMLprf}{\end{grayboxwithoutsep}}
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % for code that has line numbers
 \newenvironment{linenos}{\resetlinenumber\internallinenumbers}{\par\nolinenumbers}

Binary file progtutorial.pdf has changed