diff -r cf471fa86091 -r 615762b8d8cb ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Sat Jun 16 15:25:47 2012 +0100
+++ b/ProgTutorial/Parsing.thy	Mon Jun 18 14:49:09 2012 +0100
@@ -4,6 +4,7 @@
 
 chapter {* Parsing\label{chp:parsing} *}
 
+
 text {*
   \begin{flushright}
   {\em An important principle underlying the success and popularity of Unix\\ is
@@ -940,33 +941,16 @@
 text {*
   Often new commands, for example for providing new definitional principles,
   need to be implemented. While this is not difficult on the ML-level and
-  jEdit, in order to be compatible, new commands need also to be recognised 
-  by ProofGeneral. This results in some subtle configuration issues, which we will 
+  jEdit, in order to be backwards compatible, new commands need also to be recognised 
+  by Proof-General. This results in some subtle configuration issues, which we will 
   explain in the next section. Here we just describe how to define new commands
   to work with jEdit.
 
-  Let us start with a ``silly'' command that does nothing 
-  at all. We shall name this command \isacommand{foobar}. On the ML-level it can be 
-  defined as:
-*}
-
-ML %grayML{*let
-  val do_nothing = Scan.succeed (Local_Theory.background_theory I)
-  val kind = Keyword.thy_decl
-in
-  Outer_Syntax.local_theory ("foobar", kind) 
-    "description of foobar" 
-      do_nothing
-end *}
-
-text {*
-  The crucial function @{ML_ind local_theory in Outer_Syntax} expects a name for the command, 
-  a kind indicator (which we will explain later more thoroughly), a
-  short description and a
-  parser producing a local theory transition (its purpose will also explained
-  later). Before you can use any new command, you have to ``announce'' it in the
-  \isacommand{keyword}-section of theory header. In our running example we need
-  to write
+  Let us start with a ``silly'' command that does nothing at all. We
+  shall name this command \isacommand{foobar}.  Before you can
+  implement any new command, you have to ``announce'' it in the
+  \isacommand{keyword}-section of theory header. For \isacommand{foobar}
+  we need to write something like
 
   \begin{graybox}
   \isacommand{theory}~@{text Foo}\\
@@ -975,44 +959,71 @@
   ...
   \end{graybox}
 
-  whereby you have to declare again that the new keyword is of the appropriate
-  kind---for \isacommand{foobar} it is @{text "thy_decl"}. Another possible kind 
-  is @{text "thy_goal"} and also to omit the kind entirely, in which case you declare a 
-  keyword (something that is part of a command). After you announced the new command, 
-  you can type in your theory
+  whereby @{ML_ind "thy_decl" in Keyword} indicates the kind of the
+  command.  Another possible kind is @{text "thy_goal"}, or you can
+  also to omit the kind entirely, in which case you declare a keyword
+  (something that is part of a command).
+
+  Now you can implement \isacommand{foobar} as:
 *}
 
+ML %grayML{*let
+  val do_nothing = Scan.succeed (Local_Theory.background_theory I)
+in
+  Outer_Syntax.local_theory @{command_spec "foobar"} 
+    "description of foobar" 
+      do_nothing
+end *}
+
+text {*
+  The crucial function @{ML_ind local_theory in Outer_Syntax} expects
+  the name for the command, a kind indicator, a short description and 
+  a parser producing a local theory transition (explained later). For the
+  name and the kind, you can use the ML-antiquotation @{text "@{command_spec ...}"}.
+  After this, you can write in your theory 
+*}
+
+
 foobar
 
-text {* 
+
+text {*
+  Remember that this only works in jEdit. In order to let Proof-General 
+  recognise this command, a keyword file needs to be generated (see next
+  section).
+
   At the moment the command \isacommand{foobar} is not very useful. Let us
   refine it a bit next by letting it take a proposition as argument and
-  printing this proposition inside the tracing buffer. For this 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_ind succeed in Scan} does not parse any argument, but immediately
-  returns the simple function @{ML "Local_Theory.background_theory I"}. We can
-  replace this code by a function that first parses a proposition (using the
-  parser @{ML Parse.prop}), then prints out some tracing
-  information (using the function @{text trace_prop}) and 
-  finally does nothing. For this you can write:
+  printing this proposition inside the tracing buffer. We announce the
+  command as
+
+  \begin{graybox}
+  \isacommand{keywords} @{text [quotes] "foobar_trace"} @{text "::"} @{text "thy_decl"}
+  \end{graybox}
+
+  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 the parser @{ML_ind succeed in Scan}
+  does not parse any argument, but immediately returns the simple
+  function @{ML "Local_Theory.background_theory I"}. We can replace
+  this code by a function that first parses a proposition (using the
+  parser @{ML Parse.prop}), then prints out some tracing information
+  (using the function @{text trace_prop}) and finally does
+  nothing. For this you can write:
 *}
 
 ML %grayML{*let
   fun trace_prop str = 
     Local_Theory.background_theory (fn ctxt => (tracing str; ctxt))
-
-  val kind = Keyword.thy_decl
 in
-  Outer_Syntax.local_theory ("foobar_trace", kind) 
+  Outer_Syntax.local_theory @{command_spec "foobar_trace"} 
     "traces a proposition" 
       (Parse.prop >> trace_prop)
 end *}
 
 text {*
   The command is now \isacommand{foobar\_trace} and can be used to 
-  see the proposition in the tracing buffer (remember you need to announce
-  every new command in the header of the theory).  
+  see the proposition in the tracing buffer.
 *}
 
 foobar_trace "True \<and> False"
@@ -1030,8 +1041,14 @@
   "local_theory_to_proof" in Outer_Syntax} to set up the command. 
   Below we show the command \isacommand{foobar\_goal} which takes a
   proposition as argument and then starts a proof in order to prove
-  it. Therefore in Line 9, we set the kind indicator to @{ML thy_goal in
-  Keyword}.
+  it. Therefore, we need to announce this command in the header 
+  as @{text "thy_goal"}
+
+  \begin{graybox}
+  \isacommand{keywords} @{text [quotes] "foobar_goal"} @{text "::"} @{text "thy_goal"}
+  \end{graybox}
+
+  Then we can write:
 *}
 
 ML%linenosgray{*let
@@ -1041,10 +1058,8 @@
     in
       Proof.theorem NONE (K I) [[(prop, [])]] ctxt
     end
-  
-  val kind = Keyword.thy_goal
 in
-  Outer_Syntax.local_theory_to_proof ("foobar_goal", kind) 
+  Outer_Syntax.local_theory_to_proof @{command_spec "foobar_goal"}
     "proves a proposition" 
       (Parse.prop >> goal_prop)
 end *}
@@ -1076,6 +1091,82 @@
 done
 
 text {*
+  The final new command we describe is
+  \isacommand{foobar\_proof}. Like \isacommand{lemma}, its purpose is
+  to take a proposition and open a corresponding proof-state that
+  allows us to give a proof for it. However, unlike
+  \isacommand{lemma}, the proposition will be given as an
+  ML-value. Such a command is quite useful during development
+  of a tool that generates a goal on the ML-level and you want to see
+  whether it is provable. In addition you also want that the proved 
+  proposition can be given a lemma name that can be referenced later on.
+
+  The first problem of this new command is to parse some text as 
+  ML-source and then interpret it as a term. For the parsing we can 
+  use the function @{ML_ind "ML_source" in Parse} in the structure 
+  @{ML_struct Parse}. For running the ML-interpreter we need the 
+  following scaffolding code.
+*}
+
+ML %grayML{*
+structure Result = Proof_Data (
+  type T = unit -> term
+  fun init thy () = error "Result")
+
+val result_cookie = (Result.get, Result.put, "Result.put") *}
+
+text {*
+  With this in place we can write the code for \isacommand{foobar\_prove}.
+*}
+
+ML %linenosgray{*let
+   fun after_qed thm_name thms lthy =
+        Local_Theory.note (thm_name, (flat thms)) lthy |> snd
+
+   fun setup_proof (thm_name, (txt, pos)) lthy =
+     let
+       val trm = Code_Runtime.value lthy result_cookie ("", txt)
+     in
+       Proof.theorem NONE (after_qed thm_name) [[(trm, [])]] lthy
+     end
+
+   val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source
+in
+   Outer_Syntax.local_theory_to_proof @{command_spec "foobar_prove"}
+     "proving a proposition" 
+       (parser >> setup_proof)
+end*}
+
+text {*
+  In Line 12, we implement a parser that first reads in an optional lemma name (terminated 
+  by ``:'') and then some ML-code. The function in Lines 5 to 10 takes the ML
+  text and lets the ML-runtime evaluate it using the function @{ML_ind value in Code_Runtime}
+  in the structure @{ML_struct Code_Runtime}.  Once the ML-text has been turned into a term, 
+  the function @{ML theorem in Proof} opens a corresponding proof-state. This function takes the
+  function @{ML_text "after_qed"} as argument, whose purpose is to store the theorem,
+  once it is proven, under the user given name @{text "thm_name"}.
+
+  We can now give take a term, for example
+*}
+
+ML %grayML{*val prop_true = @{prop "True"}*}
+
+text {*
+  and give a proove for it using \isacommand{foobar\_prove}:
+*}
+
+foobar_prove test: prop_true
+apply(rule TrueI)
+done
+
+text {*
+  Finally we can test whether the lemma has been stored under the given name.
+  
+  \begin{isabelle}
+  \isacommand{thm}~@{text "test"}\\
+  @{text "> "}~@{thm TrueI}
+  \end{isabelle}
+
   While this is everything you have to do for a new command when using jEdit, 
   things are not as simple when using Emacs and ProofGeneral. We explain the details 
   next.
@@ -1113,9 +1204,8 @@
   @{ML
 "let
   val do_nothing = Scan.succeed (Local_Theory.background_theory I)
-  val kind = Keyword.thy_decl
 in
-  Outer_Syntax.local_theory (\"foobar\", kind) 
+  Outer_Syntax.local_theory @{command_spec \"foobar\"}
     \"description of foobar\" 
        do_nothing
 end"}\\
@@ -1231,38 +1321,9 @@
   
 *}
 
-ML {*
-structure Result = Proof_Data (
-  type T = unit -> term
-  fun init thy () = error "Result")
 
-val result_cookie = (Result.get, Result.put, "Result.put")
-*}
-
-ML %grayML{*let
-   fun after_qed thm_name thms lthy =
-        Local_Theory.note (thm_name, (flat thms)) lthy |> snd
 
-   fun setup_proof (thm_name, (txt, pos)) lthy =
-   let
-     val trm = Code_Runtime.value lthy result_cookie ("", txt)
-   in
-     Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy
-   end
 
-   val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source
- 
-in
-   Outer_Syntax.local_theory_to_proof ("foobar_prove", Keyword.thy_goal) 
-     "proving a proposition" 
-       (parser >> setup_proof)
-end*}
-
-(*
-foobar_prove test: {* @{prop "True"} *}
-apply(rule TrueI)
-done
-*)
 
 (*
 ML {*