# HG changeset patch # User Christian Urban # Date 1227848188 -3600 # Node ID a04bdee4fb1e6b21f97a63a49606ed840f69da67 # Parent c346c156a7cd1c16e76a44e1d7a828a9ce207314 tuned diff -r c346c156a7cd -r a04bdee4fb1e CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Fri Nov 28 05:19:55 2008 +0100 +++ b/CookBook/FirstSteps.thy Fri Nov 28 05:56:28 2008 +0100 @@ -79,8 +79,8 @@ However this only works if the type of what is converted is monomorphic and is not a function. - The funtion @{ML "warning"} should only be used for testing purposes, because any - output this funtion generates will be overwritten as soon as an error is + The function @{ML "warning"} should only be used for testing purposes, because any + output this function generates will be overwritten as soon as an error is raised. For printing anything more serious and elaborate, the function @{ML tracing} should be used. This function writes all output into a separate tracing buffer. For example @@ -89,7 +89,7 @@ It is also possible to redirect the ``channel'' where the @{ML_text "foo"} is printed to a separate file, e.g. to prevent Proof General from choking on massive - amounts of trace output. This rediretion can be achieved using the code + amounts of trace output. This redirection can be achieved using the code *} ML{* @@ -214,7 +214,7 @@ Hint: The third term is already quite big, and the pretty printer may omit parts of it by default. If you want to see all of it, you - can use the following ML funtion to set the limit to a value high + can use the following ML function to set the limit to a value high enough: \end{exercise} @@ -253,7 +253,7 @@ While antiquotations are very convenient for constructing terms and types, they can only construct fixed terms. Unfortunately, one often needs to construct terms dynamically. For example, a function that returns the implication - @{text "\(x::\). P x \ Q x"} taking @{term P}, @{term Q} and the typ @{term "\"} + @{text "\(x::\). P x \ Q x"} taking @{term P}, @{term Q} and the type @{term "\"} as arguments can only be written as *} @@ -292,7 +292,7 @@ The extra prefixes @{ML_text zero_class} and @{ML_text plus_class} are present because these constants are defined within type classes; the prefix @{text "HOL"} indicates in which theory they are defined. Guessing such internal names can sometimes be quite hard. - Therefore Isabellle provides the antiquotation @{text "@{const_name \}"} which does the + Therefore Isabelle provides the antiquotation @{text "@{const_name \}"} which does the expansion automatically, for example: @{ML_response_fake [display] "@{const_name \"Nil\"}" "List.list.Nil"} diff -r c346c156a7cd -r a04bdee4fb1e CookBook/Intro.thy --- a/CookBook/Intro.thy Fri Nov 28 05:19:55 2008 +0100 +++ b/CookBook/Intro.thy Fri Nov 28 05:56:28 2008 +0100 @@ -58,7 +58,7 @@ \end{description} The Cookbook is written in such a way that the code examples in it are - synchronised with fairly recent versions of the code. + checked against recent versions of the code. *} diff -r c346c156a7cd -r a04bdee4fb1e CookBook/Parsing.thy --- a/CookBook/Parsing.thy Fri Nov 28 05:19:55 2008 +0100 +++ b/CookBook/Parsing.thy Fri Nov 28 05:56:28 2008 +0100 @@ -45,7 +45,7 @@ @{ML_response [display] "($$ \"h\") (explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"} @{ML_response [display] "($$ \"w\") (explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"} - This function will either succeed (as in the two examples above) or raise the exeption + This function will either succeed (as in the two examples above) or raise the exception @{ML_text "FAIL"} if no string can be consumed. For example trying to parse @{ML_response_fake [display] "($$ \"x\") (explode \"world\")" @@ -68,7 +68,7 @@ Slightly more general than the parser @{ML "(op $$)"} is the function @{ML Scan.one}, in that it takes a predicate as argument and then parses exactly - one item from the input list satisfying this prediate. For example the + one item from the input list satisfying this predicate. For example the following parser either consumes an @{ML_text [quotes] "h"} or a @{ML_text [quotes] "w"}: @@ -83,7 +83,7 @@ end" "((\"h\", [\"e\", \"l\", \"l\", \"o\"]),(\"w\", [\"o\", \"r\", \"l\", \"d\"]))"} - Two parser can be connected in sequence by using the funtion @{ML "(op --)"}. + Two parser can be connected in sequence by using the function @{ML "(op --)"}. For example parsing @{ML_text "h"}, @{ML_text "e"} and @{ML_text "l"} in this sequence can be achieved by @@ -107,7 +107,7 @@ end" "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"} - The functions @{ML "(op |--)"} and @{ML "(op --|)"} work like the sequencing funtion + The functions @{ML "(op |--)"} and @{ML "(op --|)"} work like the sequencing function for parsers, except that they discard the item being parsed by the first (respectively second) parser. For example @@ -161,11 +161,11 @@ which @{ML_text p} is present in the input, but not @{ML_text q}. That means @{ML_open "(p -- q)" for p q} will fail and the - alternative parser @{ML_text r} will be tried. However in many circumstanes this will be the wrong + alternative parser @{ML_text r} will be tried. However in many circumstance this will be the wrong parser for the input ``p-followed-by-q'' and therefore will also fail. The error message is then caused by the - failure of @{ML_text r}, not by the absense of @{ML_text q} in the input. This kind of situation - can be avoided by using the funtion @{ML "(op !!)"}. This function aborts the whole process of + failure of @{ML_text r}, not by the absence of @{ML_text q} in the input. This kind of situation + can be avoided by using the function @{ML "(op !!)"}. This function aborts the whole process of parsing in case of a failure and invokes an error message. For example if we invoke the parser @{ML [display] "(!! (fn _ => \"foo\") ($$ \"h\"))"} @@ -333,7 +333,7 @@ Token (\,(Keyword, \"|\"),\), Token (\,(Keyword, \"for\"),\)]"} - we obtain a list consiting of only a command and two keyword tokens. + we obtain a list consisting of only a command and two keyword tokens. If you want to see which keywords and commands are currently known, use the following (you might have to adjust the @{ML print_depth} in order to see the complete list): diff -r c346c156a7cd -r a04bdee4fb1e CookBook/Readme.thy --- a/CookBook/Readme.thy Fri Nov 28 05:19:55 2008 +0100 +++ b/CookBook/Readme.thy Fri Nov 28 05:56:28 2008 +0100 @@ -23,17 +23,24 @@ in the implementation manual, namely \ichcite{ch:logic}. \item There are various document antiquotations defined for the - cookbook so that written text can be kept in sync with the + cookbook. This allows to check the written text against the current Isabelle code and also that responses of the ML-compiler can be shown. - The are: + Therefore authors are strongly encouraged to use antiquotations wherever + it is appropriate. + + The following antiquotations are in use: \begin{itemize} - \item[$\bullet$] {\bf @{text "@{ML \"\\"}"}} Should be used for value computations. It checks whether - the ML-expression is valid ML-code, but only works for closed expression. - \item[$\bullet$] {\bf @{text "@{ML_open \"\\" for \}"}} Works like @{ML_text ML}-antiquotation except, - that it can also deal with open expressions and expressions that need to be evaluated inside structures. - The free variables or structures need to be listed after the @{ML_text "for"}. For example + \item[$\bullet$] {\bf @{text "@{ML \"\\"}"}} Should be used for value + computations. It checks whether the ML-expression is valid ML-code, but only + works for closed expression. + + \item[$\bullet$] {\bf @{text "@{ML_open \"\\" for \}"}} Works like @{ML_text + ML}-antiquotation except, that it can also deal with open expressions and + expressions that need to be evaluated inside structures. The free variables + or structures need to be listed after the @{ML_text "for"}. For example @{text "@{ML_open \"a + b\" for a b}"}. + \item[$\bullet$] {\bf @{text "@{ML_response \"\\" \"\\"}"}} The first expression is checked like in the antiquotation @{text "@{ML \"\\"}"}; the second is a pattern that specifies the result the first expression @@ -44,17 +51,22 @@ constructed. It does not work when the code produces an exception or is an abstract datatype (like @{ML_type thm} or @{ML_type cterm}). - \item[$\bullet$] {\bf @{text "@{ML_response_fake \"\\" \"\\"}"}} Works like the - @{ML_text ML_response}-anti\-quotation, except that the result-specification is not - checked. - \item[$\bullet$] {\bf @{text "@{ML_file \"\\"}"}} Should be used when referring to a file. - It checks whether the file exists. + \item[$\bullet$] {\bf @{text "@{ML_response_fake \"\\" \"\\"}"}} Works like + the @{ML_text ML_response}-anti\-quotation, except that the + result-specification is not checked. + + \item[$\bullet$] {\bf @{text "@{ML_file \"\\"}"}} Should be used when + referring to a file. It checks whether the file exists. \end{itemize} + \item Functions and value bindings cannot be defined inside antiquotations; they need to be included inside \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} environments. Some \LaTeX-hack, however, does not print the environment markers. + \item Line numbers for code can be shown using + \isacommand{ML} \isa{\%linenumbers} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}. + \end{itemize} *} diff -r c346c156a7cd -r a04bdee4fb1e cookbook.pdf Binary file cookbook.pdf has changed