
diff -r bcbcf5c839ae -r f6f8f8ba1eb1 CookBook/Parsing.thy
--- a/CookBook/Parsing.thy	Thu Jan 15 13:42:28 2009 +0000
+++ b/CookBook/Parsing.thy	Fri Jan 16 14:57:36 2009 +0000
@@ -192,7 +192,7 @@
   see the error message properly, we need to prefix the parser with the function 
   @{ML "Scan.error"}. For example
 
-  @{ML_response_fake [display,gray] "Scan.error ((!! (fn _ => \"foo\") ($$ \"h\")))"
+  @{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"} 
@@ -557,8 +557,9 @@
   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{foobar} in what follows.
-  To keep things simple this command does nothing at all. On the ML-level it can be defined as
+  To keep things simple, 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{*let
@@ -569,22 +570,22 @@
 end *}
 
 text {*
-  The function @{ML OuterSyntax.command} expects a name for the command, a
+  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 for a top-level transition function (its purpose will also explained
+  parser producing 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 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
+  generated with the command-line:
 
 
-  @{text [display] "$ isabelle keywords -k foobar some-log-files"}
+  @{text [display] "$ isabelle keywords -k foobar 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
+  The option @{text "-k foobar"} indicates which postfix the name of the keyword file 
+  will be assigned. In the case above the generated file will be named @{text
+  "isar-keywords-foobar.el"}. As indicated, 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
@@ -617,10 +618,13 @@
   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
+  \isacommand{foobar}-command. If you target another logics besides HOL, such
+  as Nominal or ZF, then you need to adapt the log files appropriately.
+  @{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\"
@@ -635,7 +639,7 @@
 
   @{text [display] "$ isabelle mkdir FoobarCommand"}
 
-  This creates a directory containing the files 
+  This generates a directory containing the files 
 
   @{text [display] 
 "./IsaMakefile
@@ -653,18 +657,17 @@
 
   @{text [display] "$ isabelle make"}
 
-  We created finally all the necessary log files. They are typically stored 
+  We created finally all the necessary log files. They are stored 
   in the directory 
   
   @{text [display]  "~/.isabelle/heaps/Isabelle2008/polyml-5.2.1_x86-linux/log"}
 
-  or something similar depending on your Isabelle distribution and architecture. 
-  Let us assume the name of this directory is stored in the shell variable 
-  @{text "ISABELLE_LOGS"}. One way to assign this shell variable is by typing
+  or something similar depending on your Isabelle distribution and architecture.
+  One quick way to assign a shell variable to this directory is by typing
 
   @{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"}
  
-  on the Unix prompt. This directory should include the files
+  on the Unix prompt. The directory should include the files
 
   @{text [display] 
 "Pure.gz
@@ -672,21 +675,22 @@
 Pure-ProofGeneral.gz
 HOL-FoobarCommand.gz"} 
 
-  They are the ones we use for creating the keyword files. The corresponding  Unix command
-  is
+  They are the ones we need for creating the keyword files. Assuming the name 
+  of the directory is in  @{text "ISABELLE_LOGS"},
+  then the Unix command for creating the keyword file is:
 
 @{text [display]
 "$ isabelle keywords -k foobar 
      $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FoobarCommand.gz}"}
 
   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
+  string @{text "foobar"} twice (check for example that @{text "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
+  Isabelle aware of this keyword file, we have to start it with the option @{text
   "-k foobar"}, i.e.
 
-  @{text [display] "$ isabelle -k foobar a-theory-file"}
+  @{text [display] "$ isabelle -k foobar a_theory_file"}
 
   If we now run the original code
 *}
@@ -699,19 +703,17 @@
 end *}
 
 text {*
-  then we can make use of \isacommand{foobar}! Similarly with any other new command. 
+  then we can make use of \isacommand{foobar} in a theory that builds on @{text "Command.thy"}! 
+  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 adapt the
-  log files appropriately.
 
-  At the moment, \isacommand{foobar} is not very useful. Let us refine it a bit 
+  At the moment \isacommand{foobar} is not very useful. Let us next 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 
+  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 replace this code by a function that first 
   parses a proposition (using the parser @{ML OuterParse.prop}), then prints out 
@@ -729,22 +731,25 @@
 text {*
   Now we can type for example
 
-  @{ML_response_fake_both [display,gray] "foobar \"True \<and> False\"" "True \<and> False"}
+  \begin{isabelle}
+  \isacommand{foobar}~@{text [quotes] "True \<and> False"}\\
+  @{text "> True \<and> False"}
+  \end{isabelle}
   
   and see the proposition in the tracing buffer.  
 
-  Note that so far we used @{ML thy_decl in OuterKeyword} as kind indicator
+  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, however,
+  \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 (think of
   \isacommand{lemma}) or prove some other properties (for example in
-  \isacommand{function}). To achieve this behaviour we have to use the kind
+  \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 change \isacommand{foobar} so that it expects a proposition as
+  argument and then starts a proof in order to prove it. Therefore in Line 13
   below, we set the kind indicator to @{ML thy_goal in OuterKeyword}.
 *}
 
@@ -766,25 +771,30 @@
 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.
+  The function @{text set_up_thm} takes a string (the proposition to be
+  proved) and a context.  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. In Lines 9 to 11 contain the parser for the proposition.
 
-  If we now type @{text "foobar \"True \<and> True\""}, we obtain the following 
+  If we now type \isacommand{foobar}~@{text [quotes] "True \<and> True"}, we obtain the following 
   proof state:
  
-  @{ML_response_fake_both [display,gray] "foobar \"True \<and> True\"" 
-"goal (1 subgoal):
-1. True \<and> True"}
+  \begin{isabelle}
+  \isacommand{foobar}~@{text [quotes] "True \<and> False"}\\
+  @{text "goal (1 subgoal)"}\\
+  @{text "1. True \<and> True"}
+  \end{isabelle}
 
   and we can build the proof
 
-  @{text [display,gray] "foobar \"True \<and> True\"
-apply(rule conjI)
-apply(rule TrueI)+
-done"} 
+  \begin{isabelle}
+  \isacommand{foobar}~@{text [quotes] "True \<and> False"}\\
+  \isacommand{apply}@{text "(rule conjI)"}\\
+  \isacommand{apply}@{text "(rule TrueI)+"}\\
+  \isacommand{done}
+  \end{isabelle}
+
   
   (FIXME What does @{text "Toplevel.theory"}?)
 




