# HG changeset patch # User Christian Urban # Date 1231015494 0 # Node ID 5b9c6010897bfcfd1f4984f41caefcd08c55993e # Parent b5914f3c643cf4a5a440db86d4e64811411be7d7 doem tuning and made the cookbook work again with recent changes (CookBook/Package/Ind_Interface.thy needs to be looked at to see what the problem with the new parser type is) diff -r b5914f3c643c -r 5b9c6010897b CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Wed Dec 17 05:08:33 2008 +0000 +++ b/CookBook/FirstSteps.thy Sat Jan 03 20:44:54 2009 +0000 @@ -75,7 +75,7 @@ then there is a convenient, though again ``quick-and-dirty'', method for converting values into strings, for example: - @{ML_response_fake [display] "warning (makestring 1)" "1"} + @{ML_response_fake [display] "warning (makestring 1)" "\"1\""} However this only works if the type of what is converted is monomorphic and is not a function. @@ -157,7 +157,7 @@ @{ML_response_fake [display] "@{simpset}" "\"} (FIXME: what does a simpset look like? It seems to be the same problem - like tokens.) + as with tokens.) While antiquotations nowadays have many applications, they were originally introduced to avoid explicit bindings for theorems such as diff -r b5914f3c643c -r 5b9c6010897b CookBook/Intro.thy --- a/CookBook/Intro.thy Wed Dec 17 05:08:33 2008 +0000 +++ b/CookBook/Intro.thy Sat Jan 03 20:44:54 2009 +0000 @@ -9,13 +9,13 @@ The purpose of this Cookbook is to guide the reader through the first steps of Isabelle programming, and to provide recipes for solving common problems. The code provided in the Cookbook is - checked against recent versions of Isabelle. + as far as possible checked against recent versions of Isabelle. *} section {* Intended Audience and Prior Knowledge *} text {* - This cookbook targets an audience who already knows how to use Isabelle + This Cookbook targets an audience who already knows how to use Isabelle for writing theories and proofs. We also assume that readers are familiar with the functional programming language ML, the language in which most of Isabelle is implemented. If you are unfamiliar with either of diff -r b5914f3c643c -r 5b9c6010897b CookBook/Package/Ind_Interface.thy --- a/CookBook/Package/Ind_Interface.thy Wed Dec 17 05:08:33 2008 +0000 +++ b/CookBook/Package/Ind_Interface.thy Sat Jan 03 20:44:54 2009 +0000 @@ -434,14 +434,21 @@ (local_theory -> local_theory) -> Toplevel.transition -> Toplevel.transition"} which, apart from the local theory transformer, takes an optional name of a locale -to be used as a basis for the local theory. The whole parser for our command has type -@{ML_type [display] "OuterLex.token list -> +to be used as a basis for the local theory. + +(FIXME : needs to be adjusted to new parser type) + +{\it +The whole parser for our command has type +@{ML_text [display] "OuterLex.token list -> (Toplevel.transition -> Toplevel.transition) * OuterLex.token list"} -which is abbreviated by @{ML_type OuterSyntax.parser_fn}. The new command can be added +which is abbreviated by @{ML_text OuterSyntax.parser_fn}. The new command can be added to the system via the function -@{ML [display] "OuterSyntax.command : +@{ML_text [display] "OuterSyntax.command : string -> string -> OuterKeyword.T -> OuterSyntax.parser_fn -> unit"} -which imperatively updates the parser table behind the scenes. In addition to the parser, this +which imperatively updates the parser table behind the scenes. } + +In addition to the parser, this function takes two strings representing the name of the command and a short description, as well as an element of type @{ML_type OuterKeyword.T} describing which \emph{kind} of command we intend to add. Since we want to add a command for declaring new concepts, diff -r b5914f3c643c -r 5b9c6010897b CookBook/Parsing.thy --- a/CookBook/Parsing.thy Wed Dec 17 05:08:33 2008 +0000 +++ b/CookBook/Parsing.thy Sat Jan 03 20:44:54 2009 +0000 @@ -59,7 +59,7 @@ might be explored. \item @{text "MORE"} indicates that there is not enough input for the parser. For example in @{text "($$ \"h\") []"}. - \item @{text "ABORT"} is the exception which is raised when a dead end is reached. + \item @{text "ABORT"} is the exception that is raised when a dead end is reached. It is used for example in the function @{ML "(op !!)"} (see below). \end{itemize} @@ -93,7 +93,7 @@ Note how the result of consumed strings builds up on the left as nested pairs. If, as in the previous example, one wants to parse a particular string, - then one should rather use the function @{ML Scan.this_string}: + then one should use the function @{ML Scan.this_string}: @{ML_response [display] "Scan.this_string \"hel\" (explode \"hello\")" "(\"hel\", [\"l\", \"o\"])"} @@ -263,7 +263,7 @@ end of the input string. The function @{ML "Scan.unless p q" for p q} takes two parsers: if the first one can - parse the input then the whole parser fails; if not, then the second is tried. Therefore + parse the input, then the whole parser fails; if not, then the second is tried. Therefore @{ML_response_fake_both [display] "Scan.unless ($$ \"h\") ($$ \"w\") (explode \"hello\")" "Exception FAIL raised"} @@ -277,7 +277,7 @@ The functions @{ML Scan.repeat} and @{ML Scan.unless} can be combined to read any input until a certain marker symbol is reached. In the example below the marker - symbol is a @{text [quotes] "*"} which causes the parser to stop: + symbol is a @{text [quotes] "*"}. @{ML_response [display] "let @@ -315,7 +315,7 @@ end" "(\"foo bar foo\",[])"} - where the single strings in the parsed output are transformed + where the single-character strings in the parsed output are transformed back into one string. \begin{exercise}\label{ex:scancmts} diff -r b5914f3c643c -r 5b9c6010897b CookBook/Readme.thy --- a/CookBook/Readme.thy Wed Dec 17 05:08:33 2008 +0000 +++ b/CookBook/Readme.thy Sat Jan 03 20:44:54 2009 +0000 @@ -7,14 +7,14 @@ text {* \begin{itemize} - \item The cookbook can be compiled on the command-line with: + \item The Cookbook can be compiled on the command-line with: \begin{center} @{text "isabelle make"} \end{center} You very likely need a recent snapshot of Isabelle in order to compile - the cookbook. + the Cookbook. \item You can include references to other Isabelle manuals using the reference names from those manuals. To do this the following @@ -32,7 +32,7 @@ in the implementation manual, namely \ichcite{ch:logic}. \item There are various document antiquotations defined for the - cookbook. They allow to check the written text against the current + Cookbook. They allow to check the written text against the current Isabelle code and also allow to show responses of the ML-compiler. Therefore authors are strongly encouraged to use antiquotations wherever appropriate. diff -r b5914f3c643c -r 5b9c6010897b IsaMakefile --- a/IsaMakefile Wed Dec 17 05:08:33 2008 +0000 +++ b/IsaMakefile Sat Jan 03 20:44:54 2009 +0000 @@ -13,7 +13,7 @@ OUT = $(ISABELLE_OUTPUT) LOG = $(OUT)/log -USEDIR = $(ISATOOL) usedir -v true -i true -D generated +USEDIR = $(ISATOOL) usedir -v true -D generated rail: rail CookBook/generated/root diff -r b5914f3c643c -r 5b9c6010897b cookbook.pdf Binary file cookbook.pdf has changed