--- a/ProgTutorial/Parsing.thy	Sat Mar 21 12:35:03 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Mon Mar 23 12:13:33 2009 +0100
@@ -16,7 +16,7 @@
   parsing combinators. These combinators are a well-established technique for parsing, 
   which has, for example, been described in Paulson's classic ML-book \cite{paulson-ml2}.
   Isabelle developers are usually concerned with writing these outer syntax parsers, 
-  either for new definitional packages or for calling tactics with specific arguments. 
+  either for new definitional packages or for calling methods with specific arguments. 
 
   \begin{readmore}
   The library 
@@ -298,7 +298,7 @@
 
 @{ML_response [display,gray]
 "let 
-  fun double (x,y) = (x ^ x, y ^ y) 
+  fun double (x, y) = (x ^ x, y ^ y) 
 in
   (($$ \"h\") -- ($$ \"e\") >> double) (explode \"hello\")
 end"
@@ -318,6 +318,8 @@
   where the single-character strings in the parsed output are transformed
   back into one string.
  
+  (FIXME:  move to an earlier place)
+
   The function @{ML Scan.ahead} parses some input, but leaves the original
   input unchanged. For example:
 
@@ -492,8 +494,9 @@
 text {*
 
   The function @{ML "OuterParse.!!!"} can be used to force termination of the
-  parser in case of a dead end, just like @{ML "Scan.!!"} (see previous section), 
-  except that the error message is fixed to be @{text [quotes] "Outer syntax error"}
+  parser in case of a dead end, just like @{ML "Scan.!!"} (see previous section). 
+  Except that the error message of @{ML "OuterParse.!!!"} is fixed to be 
+  @{text [quotes] "Outer syntax error"}
   with a relatively precise description of the failure. For example:
 
 @{ML_response_fake [display,gray]
@@ -554,6 +557,12 @@
 
 *}
 
+section {* Context Parser (TBD) *}
+
+text {*
+  Used for example in \isacommand{attribute\_setup} and \isacommand{method\_setup}.
+*}
+
 section {* Parsing Inner Syntax *}
 
 text {*
@@ -711,6 +720,29 @@
   \end{readmore}
 *}
 
+text_raw {*
+  \begin{exercise}
+  If you look closely how @{ML SpecParse.where_alt_specs} is implemented
+  in file @{ML_file "Pure/Isar/spec_parse.ML"} and compare it to our @{ML "spec_parser"}, 
+  you can notice an additional ``tail'' (Lines 8 to 10):
+  \begin{isabelle}
+*}
+ML %linenosgray{*val spec_parser' = 
+     OuterParse.fixes -- 
+     Scan.optional
+     (OuterParse.$$$ "where" |-- 
+        OuterParse.!!! 
+          (OuterParse.enum1 "|" 
+             ((SpecParse.opt_thm_name ":" -- OuterParse.prop) --| 
+                  Scan.option (Scan.ahead (OuterParse.name || 
+                  OuterParse.$$$ "[") -- 
+                  OuterParse.!!! (OuterParse.$$$ "|"))))) [] *}
+text_raw {*
+  \end{isabelle}
+  What is the purpose of this additional ``tail''?
+  \end{exercise}
+*}
+
 section {* New Commands and Keyword Files\label{sec:newcommand} *}
 
 text {*
@@ -968,7 +1000,6 @@
   @{ML Toplevel.local_theory} do?)
 
   (FIXME read a name and show how to store theorems)
-
 *}
 
 section {* Methods *}
@@ -982,7 +1013,7 @@
 print_methods
 
 text {*
-  An example of a very simple method is the following code.
+  An example of a very simple method is:
 *}
 
 method_setup %gray foobar_meth = 
@@ -1007,6 +1038,14 @@
   \end{minipage} *}
 (*<*)oops(*>*)
 
+
+(*
+ML {* SIMPLE_METHOD *}
+ML {* METHOD *}
+ML {* K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1)) *}
+ML {* Scan.succeed  *}
+*)
+
 text {*
   (FIXME: explain a version of rule-tac)
 *}