--- a/ProgTutorial/Parsing.thy	Tue Mar 31 20:31:18 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Wed Apr 01 12:26:56 2009 +0100
@@ -195,7 +195,7 @@
   @{ML_response_fake [display,gray] "Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))"
                                "Exception Error \"foo\" raised"}
 
-  This ``prefixing'' is usually done by wrappers such as @{ML "OuterSyntax.command"} 
+  This ``prefixing'' is usually done by wrappers such as @{ML "OuterSyntax.local_theory"} 
   (see Section~\ref{sec:newcommand} which explains this function in more detail). 
   
   Let us now return to our example of parsing @{ML "(p -- q) || r" for p q
@@ -349,8 +349,6 @@
 section {* Parsing Theory Syntax *}
 
 text {*
-  (FIXME: context parser)
-
   Most of the time, however, Isabelle developers have to deal with parsing
   tokens, not strings.  These token parsers have the type:
 *}
@@ -619,12 +617,14 @@
   for inductive predicates of the form:
 *}
 
+(*
 simple_inductive
   even and odd
 where
   even0: "even 0"
 | evenS: "odd n \<Longrightarrow> even (Suc n)"
 | oddS: "even n \<Longrightarrow> odd (Suc n)"
+*)
 
 text {*
   For this we are going to use the parser:
@@ -679,7 +679,7 @@
   val input = filtered_input 
         \"foo::\\\"int \<Rightarrow> bool\\\" and bar::nat (\\\"BAR\\\" 100) and blonk\"
 in
-   parse OuterParse.fixes input
+  parse OuterParse.fixes input
 end"
 "([(foo, SOME \"\\^E\\^Ftoken\\^Eint \<Rightarrow> bool\\^E\\^F\\^E\", NoSyn), 
   (bar, SOME \"\\^E\\^Ftoken\\^Enat\\^E\\^F\\^E\", Mixfix (\"BAR\", [], 100)), 
@@ -699,10 +699,10 @@
   \end{readmore}
 
   Lines 3 to 7 in the function @{ML spec_parser} implement the parser for a
-  list of introduction rules, that is propositions with theorem
-  annotations. The introduction rules are propositions parsed by @{ML
-  OuterParse.prop}. However, they can include an optional theorem name plus
-  some attributes. For example
+  list of introduction rules, that is propositions with theorem annotations
+  such as rule names and attributes. The introduction rules are propositions
+  parsed by @{ML OuterParse.prop}. However, they can include an optional
+  theorem name plus some attributes. For example
 
 @{ML_response [display,gray] "let 
   val input = filtered_input \"foo_lemma[intro,dest!]:\"
@@ -752,8 +752,6 @@
 section {* New Commands and Keyword Files\label{sec:newcommand} *}
 
 text {*
-  (FIXME: update to the right command setup --- is this still needed?)
-
   Often new commands, for example for providing new definitional principles,
   need to be implemented. While this is not difficult on the ML-level,
   new commands, in order to be useful, need to be recognised by
@@ -766,16 +764,16 @@
 *}
 
 ML{*let
-  val do_nothing = Scan.succeed (Toplevel.theory I)
+  val do_nothing = Scan.succeed (LocalTheory.theory I)
   val kind = OuterKeyword.thy_decl
 in
-  OuterSyntax.command "foobar" "description of foobar" kind do_nothing
+  OuterSyntax.local_theory "foobar" "description of foobar" kind do_nothing
 end *}
 
 text {*
-  The crucial function @{ML OuterSyntax.command} expects a name for the command, a
-  short description, a kind indicator (which we will explain later on more thoroughly) and a
-  parser producing a top-level transition function (its purpose will also explained
+  The crucial function @{ML OuterSyntax.local_theory} expects a name for the command, a
+  short description, a kind indicator (which we will explain later more thoroughly) and a
+  parser producing a local theory transition (its purpose will also explained
   later). 
 
   While this is everything you have to do on the ML-level, you need a keyword
@@ -803,15 +801,15 @@
   \isacommand{ML}~@{text "\<verbopen>"}\\
   @{ML
 "let
-  val do_nothing = Scan.succeed (Toplevel.theory I)
+  val do_nothing = Scan.succeed (LocalTheory.theory I)
   val kind = OuterKeyword.thy_decl
 in
-  OuterSyntax.command \"foobar\" \"description of foobar\" kind do_nothing
+  OuterSyntax.local_theory \"foobar\" \"description of foobar\" kind do_nothing
 end"}\\
   @{text "\<verbclose>"}\\
   \isacommand{end}
   \end{graybox}
-  \caption{\small The file @{text "Command.thy"} is necessary for generating a log 
+  \caption{The file @{text "Command.thy"} is necessary for generating a log 
   file. This log file enables Isabelle to generate a keyword file containing 
   the command \isacommand{foobar}.\label{fig:commandtheory}}
   \end{figure}
@@ -909,25 +907,24 @@
   The crucial part of a command is the function that determines the behaviour
   of the command. In the code above we used a ``do-nothing''-function, which
   because of @{ML Scan.succeed} does not parse any argument, but immediately
-  returns the simple toplevel function @{ML "Toplevel.theory I"}. We can
+  returns the simple function @{ML "LocalTheory.theory I"}. We can
   replace this code by a function that first parses a proposition (using the
   parser @{ML OuterParse.prop}), then prints out the tracing
-  information (using a new top-level function @{text trace_top_lvl}) and 
+  information (using a new function @{text trace_prop}) and 
   finally does nothing. For this you can write:
 *}
 
 ML{*let
-  fun trace_top_lvl str = 
+  fun trace_prop str = 
      LocalTheory.theory (fn lthy => (tracing str; lthy))
 
-  val trace_prop = OuterParse.prop >> trace_top_lvl
-
+  val trace_prop_parser = OuterParse.prop >> trace_prop
   val kind = OuterKeyword.thy_decl
 in
-  OuterSyntax.local_theory "foobar" "traces a proposition" kind trace_prop
+  OuterSyntax.local_theory "foobar" "traces a proposition" 
+    kind trace_prop_parser
 end *}
 
-
 text {*
   Now you can type
 
@@ -938,17 +935,19 @@
   
   and see the proposition in the tracing buffer.  
 
-  Note that so far we used @{ML thy_decl in OuterKeyword} as the kind indicator
-  for the command.  This means that the command finishes as soon as the
-  arguments are processed. Examples of this kind of commands are
-  \isacommand{definition} and \isacommand{declare}.  In other cases,
-  commands are expected to parse some arguments, for example a proposition,
-  and then ``open up'' a proof in order to prove the proposition (for example
+  Note that so far we used @{ML thy_decl in OuterKeyword} as the kind
+  indicator for the command.  This means that the command finishes as soon as
+  the arguments are processed. Examples of this kind of commands are
+  \isacommand{definition} and \isacommand{declare}.  In other cases, commands
+  are expected to parse some arguments, for example a proposition, and then
+  ``open up'' a proof in order to prove the proposition (for example
   \isacommand{lemma}) or prove some other properties (for example
-  \isacommand{function}). To achieve this kind of behaviour, you have to use the kind
-  indicator @{ML thy_goal in OuterKeyword}.  Note, however, once you change the 
-  ``kind'' of a command from @{ML thy_decl in OuterKeyword} to @{ML thy_goal in OuterKeyword} 
-  then the keyword file needs to be re-created!
+  \isacommand{function}). To achieve this kind of behaviour, you have to use
+  the kind indicator @{ML thy_goal in OuterKeyword} and the function @{ML
+  "local_theory_to_proof" in OuterSyntax} to set up the command.  Note,
+  however, once you change the ``kind'' of a command from @{ML thy_decl in
+  OuterKeyword} to @{ML thy_goal in OuterKeyword} then the keyword file needs
+  to be re-created!
 
   Below we change \isacommand{foobar} so that it takes a proposition as
   argument and then starts a proof in order to prove it. Therefore in Line 13, 
@@ -956,34 +955,32 @@
 *}
 
 ML%linenosgray{*let
-  fun set_up_thm str ctxt =
+  fun prove_prop str ctxt =
     let
       val prop = Syntax.read_prop ctxt str
     in
       Proof.theorem_i NONE (K I) [[(prop,[])]] ctxt
     end;
   
-  val prove_prop = OuterParse.prop >>  
-      (fn str => Toplevel.print o 
-                    Toplevel.local_theory_to_proof NONE (set_up_thm str))
-  
+  val prove_prop_parser = OuterParse.prop >> prove_prop 
   val kind = OuterKeyword.thy_goal
 in
-  OuterSyntax.command "foobar" "proving a proposition" kind prove_prop
+  OuterSyntax.local_theory_to_proof "foobar" "proving a proposition" 
+    kind prove_prop_parser
 end *}
 
 text {*
-  The function @{text set_up_thm} in Lines 2 to 7 takes a string (the proposition to be
+  The function @{text prove_prop} in Lines 2 to 7 takes a string (the proposition to be
   proved) and a context as argument.  The context is necessary in order to be able to use
   @{ML Syntax.read_prop}, which converts a string into a proper proposition.
   In Line 6 the function @{ML Proof.theorem_i} starts the proof for the
   proposition. Its argument @{ML NONE} stands for a locale (which we chose to
   omit); the argument @{ML "(K I)"} stands for a function that determines what
   should be done with the theorem once it is proved (we chose to just forget
-  about it). Lines 9 to 11 contain the parser for the proposition.
+  about it). Line 9 contains the parser for the proposition.
 
   If you now type \isacommand{foobar}~@{text [quotes] "True \<and> True"}, you obtain the following 
-  proof state:
+  proof state
 
   \begin{isabelle}
   \isacommand{foobar}~@{text [quotes] "True \<and> True"}\\
@@ -991,7 +988,7 @@
   @{text "1. True \<and> True"}
   \end{isabelle}
 
-  and you can build the proof
+  and you can build the following proof
 
   \begin{isabelle}
   \isacommand{foobar}~@{text [quotes] "True \<and> True"}\\
@@ -1000,12 +997,6 @@
   \isacommand{done}
   \end{isabelle}
 
- 
-  
-  (FIXME What do @{ML "Toplevel.theory"} 
-  @{ML "Toplevel.print"} 
-  @{ML Toplevel.local_theory} do?)
-
   (FIXME read a name and show how to store theorems)
 *}