
diff -r 7ff1a681f758 -r cf471fa86091 ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Thu May 24 15:22:25 2012 +0100
+++ b/ProgTutorial/Parsing.thy	Sat Jun 16 15:25:47 2012 +0100
@@ -935,16 +935,17 @@
 *}
 
 
-section {* New Commands and Keyword Files\label{sec:newcommand} *}
+section {* New Commands\label{sec:newcommand} *}
 
 text {*
   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
-  ProofGeneral. This results in some subtle configuration issues, which we
-  will explain in this section.
+  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 
+  explain in the next section. Here we just describe how to define new commands
+  to work with jEdit.
 
-  To keep things simple, let us start with a ``silly'' command that does nothing 
+  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:
 *}
@@ -953,19 +954,142 @@
   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
+  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
+
+  \begin{graybox}
+  \isacommand{theory}~@{text Foo}\\
+  \isacommand{imports}~@{text Main}\\
+  \isacommand{keywords} @{text [quotes] "foobar"} @{text "::"} @{text "thy_decl"}\\
+  ...
+  \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
+*}
+
+foobar
+
+text {* 
+  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:
+*}
+
+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) 
+    "traces a proposition" 
+      (Parse.prop >> trace_prop)
 end *}
 
 text {*
-  The crucial function @{ML_ind local_theory in Outer_Syntax} 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). 
+  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).  
+*}
+
+foobar_trace "True \<and> False"
+
+text {*
+  Note that so far we used @{ML_ind thy_decl in Keyword} as the kind
+  indicator for the new 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_ind thy_goal in Keyword} and the function @{ML
+  "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}.
+*}
+
+ML%linenosgray{*let
+  fun goal_prop str ctxt =
+    let
+      val prop = Syntax.read_prop ctxt str
+    in
+      Proof.theorem NONE (K I) [[(prop, [])]] ctxt
+    end
+  
+  val kind = Keyword.thy_goal
+in
+  Outer_Syntax.local_theory_to_proof ("foobar_goal", kind) 
+    "proves a proposition" 
+      (Parse.prop >> goal_prop)
+end *}
 
-  While this is everything you have to do on the ML-level, you need a keyword
-  file that can be loaded by ProofGeneral. This is to enable ProofGeneral to
-  recognise \isacommand{foobar} as a command. Such a keyword file can be
-  generated with the command-line:
+text {*
+  The function @{text goal_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_ind read_prop in Syntax}, which converts a string into a proper proposition.
+  In Line 6 the function @{ML_ind theorem in Proof} 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). 
+
+  If you now type \isacommand{foobar\_goal}~@{text [quotes] "True \<and> True"},
+  you obtain the following proof state:
+*}
+
+foobar_goal "True \<and> True"
+txt {*
+  \begin{minipage}{\textwidth}
+  @{subgoals [display]}
+  \end{minipage}\medskip
+
+  and can prove the proposition as follows.
+*}
+apply(rule conjI)
+apply(rule TrueI)+
+done
+
+text {*
+  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.
+*}
+
+
+section {* Proof-General and Keyword Files *}
+
+text {*
+  In order to use a new command in Emacs and Proof-General, you need a keyword
+  file that can be loaded by ProofGeneral. To keep things simple we take as
+  running example the command \isacommand{foobar} from the previous section. 
+
+  A keyword file can be generated with the command-line:
 
   @{text [display] "$ isabelle keywords -k foobar some_log_files"}
 
@@ -983,6 +1107,7 @@
   \begin{graybox}\small
   \isacommand{theory}~@{text Command}\\
   \isacommand{imports}~@{text Main}\\
+  \isacommand{keywords} @{text [quotes] "foobar"} @{text "::"} @{text "thy_decl"}\\
   \isacommand{begin}\\
   \isacommand{ML}~@{text "\<verbopen>"}\\
   @{ML
@@ -990,7 +1115,9 @@
   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
+  Outer_Syntax.local_theory (\"foobar\", kind) 
+    \"description of foobar\" 
+       do_nothing
 end"}\\
   @{text "\<verbclose>"}\\
   \isacommand{end}
@@ -1046,7 +1173,7 @@
   If the compilation succeeds, you have finally created all the necessary log files. 
   They are stored in the directory 
   
-  @{text [display]  "~/.isabelle/heaps/Isabelle2009/polyml-5.2.1_x86-linux/log"}
+  @{text [display]  "~/.isabelle/heaps/Isabelle2012/polyml-5.2.1_x86-linux/log"}
 
   or something similar depending on your Isabelle distribution and architecture.
   One quick way to assign a shell variable to this directory is by typing
@@ -1081,114 +1208,22 @@
   @{text [display] "$ isabelle emacs -k foobar a_theory_file"}
 
   If you now build a theory on top of @{text "Command.thy"}, 
-  then you can use the command \isacommand{foobar}. You can just write
-*}
-
-foobar
+  then you can now use the command \isacommand{foobar}
+  in Proof-General
 
-text {* 
-  but you will not see any action as we chose to implement this command to do
-  nothing. The point of this command is only to show the procedure of how
-  to interact with ProofGeneral. A similar procedure has to be done with any 
+  A similar procedure has to be done with any 
   other new command, and also any new keyword that is introduced with 
   the function @{ML_ind define in Keyword}. For example:
 *}
 
 ML %grayML{*val _ = Keyword.define ("blink", NONE) *}
 
-text {*
-  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.
-
-  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 the tracing
-  information (using a new 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) "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.  
-*}
-
-foobar_trace "True \<and> False"
 
 text {*
-  Note that so far we used @{ML_ind thy_decl in Keyword} 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_ind thy_goal in Keyword} and the function @{ML
-  "local_theory_to_proof" in Outer_Syntax} to set up the command.  Note,
-  however, once you change the ``kind'' of a command from @{ML thy_decl in
-  Keyword} to @{ML thy_goal in Keyword} then the keyword file needs
-  to be re-created!
-
-  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}.
+  Also if the kind of a command changes, from @{text "thy_decl"} to 
+  @{text "thy_goal"} say,  you need to recreate the keyword file.
 *}
 
-ML%linenosgray{*let
-  fun goal_prop str lthy =
-    let
-      val prop = Syntax.read_prop lthy str
-    in
-      Proof.theorem NONE (K I) [[(prop, [])]] lthy
-    end
-  
-  val kind = Keyword.thy_goal
-in
-  Outer_Syntax.local_theory_to_proof ("foobar_goal", kind) "proves a proposition" 
-    (Parse.prop >> goal_prop)
-end *}
-
-text {*
-  The function @{text goal_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_ind read_prop in Syntax}, which converts a string into a proper proposition.
-  In Line 6 the function @{ML_ind theorem in Proof} 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). Line 9 contains the parser for the proposition.
-
-  If you now type \isacommand{foobar\_goal}~@{text [quotes] "True \<and> True"},
-  you obtain the following proof state
-*}
-
-foobar_goal "True \<and> True"
-txt {*
-  \begin{minipage}{\textwidth}
-  @{subgoals [display]}
-  \end{minipage}\medskip
-
-  and can prove the proposition as follows.
-*}
-apply(rule conjI)
-apply(rule TrueI)+
-done
-
 text {*
   {\bf TBD below}
 
@@ -1197,7 +1232,7 @@
 *}
 
 ML {*
-structure Result = Proof_Data(
+structure Result = Proof_Data (
   type T = unit -> term
   fun init thy () = error "Result")
 
@@ -1398,13 +1433,15 @@
   \end{minipage} *}
 (*<*)oops(*>*)
 
-method_setup test = {* Scan.lift (Scan.succeed (K Method.succeed)) *} {* bla *}
+method_setup test = {* 
+  Scan.lift (Scan.succeed (K Method.succeed)) *} {* bla *}
 
 lemma "True"
 apply(test)
 oops
 
-method_setup joker = {* Scan.lift (Scan.succeed (fn ctxt => Method.cheating true ctxt)) *} {* bla *}
+method_setup joker = {* 
+  Scan.lift (Scan.succeed (fn ctxt => Method.cheating true ctxt)) *} {* bla *}
 
 lemma "False"
 apply(joker)




