isabelle-cookbook: comparison CookBook/Parsing.thy

equal deleted inserted replaced

-:d563f8ff6aa0
+:5fbeeac2901b
 need to be programmed. While this is not difficult to do 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, below named \isacommand{foo}, which does nothing at all.
+Let us start with a ``silly'' command, which we call \isacommand{foo} in what follows.
-On the ML-level it can be defined as
+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
 in
 OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing
 end"}
 The function @{ML OuterSyntax.command} expects a name for the command, a
-short description, a flag (which we will explain it later on more thoroughly) and a
+short description, a flag (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
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 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 command. @{text Pure} and @{text HOL} are usually compiled during the
+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
 @{text [display]
 "$ ./build -m \"Pure\"
 We need to copy the file @{text "Command.thy"} into the directory @{text "FooCommand"}
 and add the line
 @{text [display] "use_thy \"Command\";"}
-to the file @{text "./FooCommand/ROOT.ML"}. Now we can compile the theory by just typing
+to the file @{text "./FooCommand/ROOT.ML"}. We can now compile the theory by just typing
 @{text [display] "$ isabelle make"}
-We created now the necessary log files. They are typically stored
+We created finally all the necessary log files. They are typically 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.
 "Pure.gz
 HOL.gz
 Pure-ProofGeneral.gz
 HOL-FooCommand.gz"}
-We can now create the keyword file with
+They are used for creating the keyword files with the command
 @{text [display]
 "$ isabelle keywords -k foo
-`$ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral,HOL-FooCommand.gz}`"}
+$ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FooCommand.gz}"}
-The result is the file @{text "isar-keywords-foo.el"}, which needs to be
+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 need to start it with the option @{text "-k foo"}, i.e.
+this keyword file, we have to start it with the option @{text "-k foo"}, i.e.
 @{text [display] "isabelle -k foo <a-theory-file>"}
 If we now run the original code
 val flag = OuterKeyword.thy_decl
 in
 OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing
 end"}
-then we can finally make use of \isacommand{foo}! Similarly
+then we can make use of \isacommand{foo}! Similarly with any other new command.
-with any other command you want to implement.
 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
 log files appropriately.

changeset 67	5fbeeac2901b
parent 66	d563f8ff6aa0
child 68	e7519207c2b7