# HG changeset patch # User Christian Urban # Date 1232972983 0 # Node ID 95e9c4556221be4915a720cf8ff2a18b17f48df5 # Parent a53c7810e38bbfcb7511b9814bfd8d93e2464b59 tuned diff -r a53c7810e38b -r 95e9c4556221 CookBook/Base.thy --- a/CookBook/Base.thy Mon Jan 26 12:29:01 2009 +0000 +++ b/CookBook/Base.thy Mon Jan 26 12:29:43 2009 +0000 @@ -15,4 +15,5 @@ Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt)))); *} + end diff -r a53c7810e38b -r 95e9c4556221 CookBook/Intro.thy --- a/CookBook/Intro.thy Mon Jan 26 12:29:01 2009 +0000 +++ b/CookBook/Intro.thy Mon Jan 26 12:29:43 2009 +0000 @@ -11,10 +11,8 @@ of Isabelle programming, and to explain tricks of the trade. The code provided in the Cookbook is as far as possible checked against recent versions of Isabelle. If something does not work, then please let us - know. If you have comments or like to add to the Cookbook, you are very - welcome! The Cookbook will {\bf only} remain to be helpful, if it gets constantly - updated. - + know. If you have comments or like to add to the Cookbook, + feel free--you are very welcome! *} section {* Intended Audience and Prior Knowledge *} @@ -64,11 +62,12 @@ *} -section {* Conventions *} +section {* Conventions in the Cookbook *} text {* - All ML-code in this Cookbook is shown in highlighed displays, such as: + All ML-code in this Cookbook is shown in highlighed displays, like the following + ML-expression. \begin{isabelle} \begin{graybox} @@ -82,25 +81,26 @@ This corresponds to how code can be processed inside the interactive environment of Isabelle. However, for better readability we will drop the enclosing \isacommand{ML} \isa{\isacharverbatimopen \ldots - \isacharverbatimclose} and just show + \isacharverbatimclose} and just write @{ML [display,gray] "3 + 4"} - for the code above. Whenever appropriate we show the response of the code - when evaluated. The response is prefixed with a @{text [quotes] ">"}", like + for the code above. Whenever appropriate we also show the response of the code + when evaluated. The response is prefixed with a @{text [quotes] ">"}" like @{ML_response [display,gray] "3 + 4" "7"} - Isabelle commands are written in bold. For example \isacommand{lemma}, - \isacommand{foobar} and so on. We use @{text "$"} to indicate a command - needs to be run on the Unix-command line, like + Isabelle commands are written in bold, for example \isacommand{lemma}, + \isacommand{foobar} and so on. We use @{text "$"} to indicate that + a command needs to be run on the Unix-command line, for example @{text [display] "$ ls -la"} - Pointers to further information and files are indicated as follows: + Pointers to further information and Isabelle files are highlighted + as follows: \begin{readmore} - Further information. + Further information or pointer to file. \end{readmore} *} diff -r a53c7810e38b -r 95e9c4556221 CookBook/Parsing.thy --- a/CookBook/Parsing.thy Mon Jan 26 12:29:01 2009 +0000 +++ b/CookBook/Parsing.thy Mon Jan 26 12:29:43 2009 +0000 @@ -580,11 +580,10 @@ 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"} 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 + will be assigned. In the case above the file will be named @{text "isar-keywords-foobar.el"}. As can be seen, 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 @@ -608,7 +607,7 @@ end"}\\ \isa{\isacharverbatimclose}\\ \isacommand{end} - \end{graybox}\\[-4mm] + \end{graybox} \caption{\small 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{foobar}.\label{fig:commandtheory}} @@ -681,15 +680,17 @@ @{text [display] "$ isabelle keywords -k foobar - $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FoobarCommand.gz}"} + $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 "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 aware of this keyword file, we have to start Isabelle with the option @{text + The result is the file @{text "isar-keywords-foobar.el"}. It should contain + the string @{text "foobar"} twice (to see whether things went wrong, check + that @{text "grep foobar"} on this file returns something + non-empty). This keyword file needs to + be copied into the directory @{text "~/.isabelle/etc"}. To make Isabelle + aware of this keyword file, we have to start Isabelle with the option @{text "-k foobar"}, i.e. + @{text [display] "$ isabelle -k foobar a_theory_file"} If we now build a theory on top of @{text "Command.thy"}, @@ -779,7 +780,7 @@ proof state: \begin{isabelle} - \isacommand{foobar}~@{text [quotes] "True \ False"}\\ + \isacommand{foobar}~@{text [quotes] "True \ True"}\\ @{text "goal (1 subgoal)"}\\ @{text "1. True \ True"} \end{isabelle} @@ -787,7 +788,7 @@ and we can build the proof \begin{isabelle} - \isacommand{foobar}~@{text [quotes] "True \ False"}\\ + \isacommand{foobar}~@{text [quotes] "True \ True"}\\ \isacommand{apply}@{text "(rule conjI)"}\\ \isacommand{apply}@{text "(rule TrueI)+"}\\ \isacommand{done} @@ -796,14 +797,13 @@ (FIXME What does @{text "Toplevel.theory"} @{text "Toplevel.print"}?) - (FIXME Explain @{text "OuterKeyword.thy_decl"} and parser) - (FIXME read a name and show how to store theorems) (FIXME possibly also read a locale) *} (*<*) + chapter {* Parsing *} text {* @@ -1472,5 +1472,4 @@ *} (*>*) - end \ No newline at end of file diff -r a53c7810e38b -r 95e9c4556221 CookBook/Solutions.thy --- a/CookBook/Solutions.thy Mon Jan 26 12:29:01 2009 +0000 +++ b/CookBook/Solutions.thy Mon Jan 26 12:29:43 2009 +0000 @@ -41,11 +41,14 @@ @{ML scan_all} retruns a string, instead of the pair a parser would normally return. For example: - @{ML_response [display,gray] "scan_all (explode \"foo bar\")" "\"foo bar\""} - - @{ML_response [display,gray] "scan_all (explode \"foo (*test*) bar (*test*)\")" - "\"foo (**test**) bar (**test**)\""} - + @{ML_response [display,gray] +"let + val input1 = (explode \"foo bar\") + val input2 = (explode \"foo (*test*) bar (*test*)\") + in + (scan_all input1, scan_all input2) + end" +"(\"foo bar\",\"foo (**test**) bar (**test**)\")"} *} end \ No newline at end of file diff -r a53c7810e38b -r 95e9c4556221 cookbook.pdf Binary file cookbook.pdf has changed