
diff -r 5fbeeac2901b -r e7519207c2b7 CookBook/Parsing.thy
--- a/CookBook/Parsing.thy	Mon Jan 12 16:49:15 2009 +0000
+++ b/CookBook/Parsing.thy	Wed Jan 14 16:46:07 2009 +0000
@@ -1,5 +1,5 @@
 theory Parsing
-imports Base
+imports Base 
 
 begin
 
@@ -556,70 +556,78 @@
 section {* New Commands and Creating Keyword Files *}
 
 text {*
-  Often new commands, for example for providing a new definitional principle,
-  need to be programmed. While this is not difficult to do on the ML-level,
+  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.
 
-  Let us start with a ``silly'' command, which we call \isacommand{foo} in what follows.
+  Let us start with a ``silly'' command, which we call \isacommand{foobar} in what follows.
   To keep things simple this command does nothing at all. On the ML-level it can be defined as
+*}
 
-@{ML [display]
-"let
-  val do_nothing = Scan.succeed (Toplevel.theory (fn x => x))
-  val flag = OuterKeyword.thy_decl
+ML {* 
+let
+  val do_nothing = Scan.succeed (Toplevel.theory I)
+  val kind = OuterKeyword.thy_decl
 in
-  OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing
-end"}
+  OuterSyntax.command "foobar" "description of foobar" kind do_nothing
+end 
+*}
 
+text {*
   The function @{ML OuterSyntax.command} expects a name for the command, a
-  short description, a flag (which we will explain later on more thoroughly) and a
+  short description, a kind indicator (which we will explain later on more thoroughly) and a
   parser for a top-level transition function (its purpose will also explained
   later). 
 
-  While this is everything we have to do on the ML-level, we need 
-  now a keyword file that can be loaded by ProofGeneral. This is to enable ProofGeneral 
-  to recognise  \isacommand{foo} as a command. Such a keyword file can be generated with 
-  the command-line
+  While this is everything we have to do on the ML-level, we 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 [display] "$ isabelle keywords -k foobar some-log-files"}
 
-  @{text [display] "$ isabelle keywords -k foo <some-log-files>"}
+  The option @{text "-k foobar"} indicates which postfix the keyword file will
+  obtain. In the case above the generated file will be named @{text
+  "isar-keywords-foobar.el"}. However, this command requires log files to be
+  present (in order to extract the keywords from them). To generate these log
+  files, we first package the code above into a separate theory file named
+  @{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the
+  complete code.
 
-  The option @{text "-k foo"} indicates which postfix the keyword file will obtain. In
-  the case above the generated file will be named @{text "isar-keywords-foo.el"}. This command
-  requires log files to be present (in order to extract the keywords from them). 
-  To generate these log files, we first package the code above into a separate theory file 
-  named @{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the complete code. 
 
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \begin{figure}[t]
-  \begin{boxedminipage}{\textwidth}
+  \begin{boxedminipage}{\textwidth}\small
   \isacommand{theory}~@{text Command}\\
   \isacommand{imports}~@{text Main}\\
   \isacommand{begin}\\
   \isacommand{ML}~\isa{\isacharverbatimopen}\\
   @{ML
 "let
-  val do_nothing = Scan.succeed (Toplevel.theory (fn x => x))
-  val flag = OuterKeyword.thy_decl
+  val do_nothing = Scan.succeed (Toplevel.theory I)
+  val kind = OuterKeyword.thy_decl
 in
-  OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing
+  OuterSyntax.command \"foobar\" \"description of foobar\" kind do_nothing
 end"}\\
   \isa{\isacharverbatimclose}\\
   \isacommand{end}
   \end{boxedminipage}
   \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{foo}.\label{fig:commandtheory}}
+  the command \isacommand{foobar}.\label{fig:commandtheory}}
   \end{figure}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-  For 
-  our purposes it is sufficient to use the log files for the theories @{text "Pure"},
-  @{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as the theory @{text "Command.thy"}
-  containing the new \isacommand{foo}-command. @{text Pure} and @{text HOL} are usually compiled during the 
-  installation of Isabelle. So log files for them are already available. If not, then they 
-  can be conveniently compiled using build-script from the distribution
+  For our purposes it is sufficient to use the log files for the theories
+  @{text "Pure"}, @{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as
+  the theory @{text "Command.thy"} containing the new
+  \isacommand{foobar}-command. @{text Pure} and @{text HOL} are usually
+  compiled during the installation of Isabelle. So log files for them should be
+  already available. If not, then they can be conveniently compiled using
+  build-script from the Isabelle distribution
 
   @{text [display] 
 "$ ./build -m \"Pure\"
@@ -632,23 +640,23 @@
   For the theory @{text "Command.thy"}, we first create a ``managed'' subdirectory 
   with
 
-  @{text [display] "$ isabelle mkdir FooCommand"}
+  @{text [display] "$ isabelle mkdir FoobarCommand"}
 
   This creates a directory containing the files 
 
   @{text [display] 
 "./IsaMakefile
-./FooCommand/ROOT.ML
-./FooCommand/document
-./FooCommand/document/root.tex"}
+./FoobarCommand/ROOT.ML
+./FoobarCommand/document
+./FoobarCommand/document/root.tex"}
 
 
-  We need to copy the file @{text "Command.thy"} into the directory @{text "FooCommand"}
+  We need to copy the file @{text "Command.thy"} into the directory @{text "FoobarCommand"}
   and add the line 
 
   @{text [display] "use_thy \"Command\";"} 
   
-  to the file @{text "./FooCommand/ROOT.ML"}. We can now compile the theory by just typing
+  to the file @{text "./FoobarCommand/ROOT.ML"}. We can now compile the theory by just typing
 
   @{text [display] "$ isabelle make"}
 
@@ -663,50 +671,139 @@
 
   @{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"}
  
-  In this directory are the files
+  on the Unix prompt. This directory should include the files
 
   @{text [display] 
 "Pure.gz
 HOL.gz
 Pure-ProofGeneral.gz
-HOL-FooCommand.gz"} 
+HOL-FoobarCommand.gz"} 
 
-  They are used for creating the keyword files with the command
+  They are the ones we use for creating the keyword files. The corresponding  Unix command
+  is
 
 @{text [display]
-"$ isabelle keywords -k foo 
-       $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FooCommand.gz}"}
+"$ isabelle keywords -k foobar 
+     $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FoobarCommand.gz}"}
 
-  The result is the file @{text "isar-keywords-foo.el"}. This file needs to be 
-  copied to the directory @{text "~/.isabelle/etc"}. To make Isabelle use
-  this keyword file, we have to start it with the option @{text "-k foo"}, i.e.
+  The result is the file @{text "isar-keywords-foobar.el"}. It should contain the
+  string @{text "foobar"} twice (check for example that @{text [quotes] "grep foobar
+  isar-keywords-foobar.el"} returns something non-empty).  This keyword file
+  needs to be copied into the directory @{text "~/.isabelle/etc"}. To make
+  Isabelle use this keyword file, we have to start it with the option @{text
+  "-k foobar"}, i.e.
 
-  @{text [display] "isabelle -k foo <a-theory-file>"}
+  @{text [display] "$ isabelle -k foobar a-theory-file"}
 
   If we now run the original code
+*}
 
-  @{ML [display]
-"let
-  val do_nothing = Scan.succeed (Toplevel.theory (fn x => x))
-  val flag = OuterKeyword.thy_decl
+ML {*
+let
+  val do_nothing = Scan.succeed (Toplevel.theory I)
+  val kind = OuterKeyword.thy_decl
 in
-  OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing
-end"}
+  OuterSyntax.command "foobar" "description of foobar" kind do_nothing
+end 
+*}
 
-  then we can make use of \isacommand{foo}! Similarly with any other new command. 
+text {*
+  then we can make use of \isacommand{foobar}! Similarly with any other new command. 
 
   In the example above, we built the theories on top of the HOL-logic. If you
-  target other logics, such as Nominal or ZF, then you need to change the
+  target other logics, such as Nominal or ZF, then you need to adapt the
   log files appropriately.
 
+  At the moment, \isacommand{foobar} is not very useful. Let us refine it a bit 
+  by taking 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 the the 
+  @{text 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 replace this code by a function that first 
+  parses a proposition (using the parser @{ML OuterParse.prop}), then prints out 
+  the tracing information and finally does nothing. For this we can write
+*}
+
+ML {* 
+let
+  val trace_prop = 
+         OuterParse.prop >> (fn str => (tracing str; (Toplevel.theory I)))
+  val kind = OuterKeyword.thy_decl
+in
+  OuterSyntax.command "foobar" "traces a proposition" kind trace_prop
+end 
+*}
+
+text {*
+  Now we can type for example
+
+  @{ML_response_fake_both [display] "foobar \"True \<and> False\"" "True \<and> False"}
+  
+  and see the proposition in the tracing buffer.  
+
+  Note that so far we used @{ML thy_decl in OuterKeyword} as 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, however,
+  commands are expected to parse some arguments, for example a proposition,
+  and then ``open up'' a proof in order to prove the proposition (think of
+  \isacommand{lemma}) or prove some other properties (for example in
+  \isacommand{function}). To achieve this behaviour we have to use the kind
+  indicator @{ML thy_goal in OuterKeyword}.
+
+  Below we change \isacommand{foobar} is such a way that an proposition as
+  argument and then start a proof in order to prove it. Therefore in Line 13
+  below, we set the kind indicator to @{ML thy_goal in OuterKeyword}.
+*}
+
+ML %linenumbers {*let
+  fun set_up_thm str ctxt =
+    let
+      val prop = Syntax.read_prop ctxt str
+    in
+      Proof.theorem_i NONE (K I) [[(Syntax.read_prop ctxt str,[])]] ctxt
+    end;
+  
+  val prove_prop = OuterParse.prop >>  
+      (fn str => Toplevel.print o 
+                    Toplevel.local_theory_to_proof NONE (set_up_thm str))
+  
+  val kind = OuterKeyword.thy_goal
+in
+  OuterSyntax.command "foobar" "proving a proposition" kind prove_prop
+end 
+*}
+
+text {*
+  The function @{text set_up_thm} takes a string (the proposition) and a context.
+  The context is necessary in order to convert the string into a proper proposition
+  using the function @{ML Syntax.read_prop}. In Line 6 we use the function
+  @{ML Proof.theorem_i} to start the proof for the proposition. In Lines 9 to
+  11 contain the parser for the proposition.
+
+  If we now type @{text "foobar \"True \<and> True\""}, we obtain the following 
+  proof state:
+ 
+  @{ML_response_fake_both [display] "foobar \"True \<and> True\"" 
+"goal (1 subgoal):
+1. True \<and> True"}
+
+  and we can build the proof
+
+  @{text [display] "foobar \"True \<and> True\"
+apply(rule conjI)
+apply(rule TrueI)+
+done"} 
+  
+  (FIXME What does @{text "Toplevel.theory"}?)
+
   (FIXME Explain @{text "OuterKeyword.thy_decl"} and parser)
-  
 
 *}
 
-
-
-
 chapter {* Parsing *}
 
 text {*




