isabelle-cookbook: comparison CookBook/Parsing.thy

equal deleted inserted replaced

-:bcbcf5c839ae
+:f6f8f8ba1eb1
 then the parsing aborts and the error message @{text "foo"} is printed out. In order to
 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"}
 (FIXME: give reference to later place).
 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{foobar} in what follows.
+To keep things simple, let us start with a ``silly'' command that does nothing
-To keep things simple this command does nothing at all. On the ML-level it can be defined as
+at all. We shall name this command \isacommand{foobar}. On the ML-level it can be
+defined as
 *}
 ML{*let
 val do_nothing = Scan.succeed (Toplevel.theory I)
 val kind = OuterKeyword.thy_decl
 in
 OuterSyntax.command "foobar" "description of foobar" kind do_nothing
 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
+The option @{text "-k foobar"} indicates which postfix the name of the keyword file
-obtain. In the case above the generated file will be named @{text
+will be assigned. In the case above the generated file will be named @{text
-"isar-keywords-foobar.el"}. However, this command requires log files to be
+"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
 complete code.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 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
+\isacommand{foobar}-command. If you target another logics besides HOL, such
-compiled during the installation of Isabelle. So log files for them should be
+as Nominal or ZF, then you need to adapt the log files appropriately.
-already available. If not, then they can be conveniently compiled using
+@{text Pure} and @{text HOL} are usually compiled during the installation of
-build-script from the Isabelle distribution
+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\"
 $ ./build -m \"HOL\""}
 For the theory @{text "Command.thy"}, we first create a ``managed'' subdirectory
 with
 @{text [display] "$ isabelle mkdir FoobarCommand"}
-This creates a directory containing the files
+This generates a directory containing the files
 @{text [display]
 "./IsaMakefile
 ./FoobarCommand/ROOT.ML
 ./FoobarCommand/document
 to the file @{text "./FoobarCommand/ROOT.ML"}. We can now compile the theory by just typing
 @{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
+One quick way to assign a shell variable to this directory is by typing
-@{text "ISABELLE_LOGS"}. One way to assign this shell variable 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
 HOL.gz
 Pure-ProofGeneral.gz
 HOL-FoobarCommand.gz"}
-They are the ones we use for creating the keyword files. The corresponding  Unix command
+They are the ones we need for creating the keyword files. Assuming the name
-is
+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
 *}
 ML{*let
 in
 OuterSyntax.command "foobar" "description of foobar" kind do_nothing
 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 next refine it a bit
-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
+the behaviour of the command. In the code above we used a
-@{text do_nothing}-function, which because of @{ML Scan.succeed} does not parse
+``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
 *}
 end *}
 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
+Below we change \isacommand{foobar} so that it expects a proposition as
-argument and then start a proof in order to prove it. Therefore in Line 13
+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}.
 *}
 ML%linenumbers{*let
 fun set_up_thm str ctxt =
 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 function @{text set_up_thm} takes a string (the proposition to be
-The context is necessary in order to convert the string into a proper proposition
+proved) and a context.  The context is necessary in order to be able to use
-using the function @{ML Syntax.read_prop}. In Line 6 we use the function
+@{ML Syntax.read_prop}, which converts a string into a proper proposition.
-@{ML Proof.theorem_i} to start the proof for the proposition. In Lines 9 to
+In Line 6 the function @{ML Proof.theorem_i} starts the proof for the
-11 contain the parser for the proposition.
+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\""
+\begin{isabelle}
-"goal (1 subgoal):
+\isacommand{foobar}~@{text [quotes] "True \<and> False"}\\
-1. True \<and> True"}
+@{text "goal (1 subgoal)"}\\
+@{text "1. True \<and> True"}
+\end{isabelle}
 and we can build the proof
-@{text [display,gray] "foobar \"True \<and> True\"
+\begin{isabelle}
-apply(rule conjI)
+\isacommand{foobar}~@{text [quotes] "True \<and> False"}\\
-apply(rule TrueI)+
+\isacommand{apply}@{text "(rule conjI)"}\\
-done"}
+\isacommand{apply}@{text "(rule TrueI)+"}\\
+\isacommand{done}
+\end{isabelle}
 (FIXME What does @{text "Toplevel.theory"}?)
 (FIXME Explain @{text "OuterKeyword.thy_decl"} and parser)

changeset 74	f6f8f8ba1eb1
parent 72	7b8c4fe235aa
child 75	f2dea0465bb4