# HG changeset patch # User Christian Urban # Date 1231778955 0 # Node ID 5fbeeac2901b1328733b4ff9fe4742e430e037d2 # Parent d563f8ff6aa0b594db6b0ba2f1edad3256d90b65 tuned diff -r d563f8ff6aa0 -r 5fbeeac2901b CookBook/Parsing.thy --- a/CookBook/Parsing.thy Mon Jan 12 16:03:05 2009 +0000 +++ b/CookBook/Parsing.thy Mon Jan 12 16:49:15 2009 +0000 @@ -562,8 +562,8 @@ 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. - On the ML-level it can be defined as + Let us start with a ``silly'' command, which we call \isacommand{foo} 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 @@ -574,7 +574,7 @@ 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). @@ -617,7 +617,7 @@ 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 @@ -648,11 +648,11 @@ @{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"} @@ -671,15 +671,15 @@ 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 "} @@ -693,8 +693,7 @@ OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing end"} - then we can finally make use of \isacommand{foo}! Similarly - with any other command you want to implement. + then we can make use of \isacommand{foo}! 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 diff -r d563f8ff6aa0 -r 5fbeeac2901b CookBook/Recipes/Config.thy --- a/CookBook/Recipes/Config.thy Mon Jan 12 16:03:05 2009 +0000 +++ b/CookBook/Recipes/Config.thy Mon Jan 12 16:49:15 2009 +0000 @@ -14,7 +14,7 @@ Assume you want to control three values, say @{ML_text bval} containing a boolean, @{ML_text ival} containing an integer and @{ML_text sval} - containing a string. These values can be declared on the ML-level by + containing a string. These values can be declared on the ML-level with *} ML {* @@ -24,7 +24,7 @@ *} text {* - where each value is given a default. To enable these values, they need to + where each value needs to be given a default. To enable these values, they need to be set up using *} @@ -38,13 +38,13 @@ *} text {* - The user can now manipulate the values with the command + The user can now manipulate the values from within Isabelle with the command *} declare [[bval = true, ival = 3]] text {* - from within Isabelle. On the ML-level these values can be retrieved using the + On the ML-level these values can be retrieved using the function @{ML Config.get}: @{ML_response [display] "Config.get @{context} bval" "true"} diff -r d563f8ff6aa0 -r 5fbeeac2901b CookBook/Recipes/TimeLimit.thy --- a/CookBook/Recipes/TimeLimit.thy Mon Jan 12 16:03:05 2009 +0000 +++ b/CookBook/Recipes/TimeLimit.thy Mon Jan 12 16:49:15 2009 +0000 @@ -11,7 +11,7 @@ {\bf Solution:} This can be achieved using the function @{ML timeLimit in TimeLimit}.\smallskip - Assume the following well-known function: + Assume the following infamous function: *} @@ -27,7 +27,7 @@ @{ML_response_fake [display] "ackermann (4, 12)" "\"} - takes a bit long. To avoid this, the call can be encapsulated + takes a bit of time to finish. To avoid this, the call can be encapsulated in a time limit of five seconds. For this you have to write: @{ML_response [display] diff -r d563f8ff6aa0 -r 5fbeeac2901b cookbook.pdf Binary file cookbook.pdf has changed