# HG changeset patch # User Christian Urban # Date 1229448485 0 # Node ID f3794c231898400e9fcda3b59968a68efa8eeb60 # Parent 065f472c09ab244d3187f833b778d11c0d69b50f fixed typos diff -r 065f472c09ab -r f3794c231898 CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Tue Dec 16 17:37:39 2008 +0100 +++ b/CookBook/FirstSteps.thy Tue Dec 16 17:28:05 2008 +0000 @@ -33,15 +33,16 @@ \isacharverbatimopen\isanewline \hspace{5mm}@{ML "3 + 4"}\isanewline \isacharverbatimclose\isanewline -@{ML_text "> 7"}\smallskip} +@{text "> 7"}\smallskip} - Expressions inside \isacommand{ML}-commands are immediately evaluated, - like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of + The @{text [quotes] "> 7"} indicates the response Isabelle prints out when the + \isacommand{ML}-command is evaluated. Like ``normal'' Isabelle proof scripts, + \isacommand{ML}-commands can be evaluated by using the advance and undo buttons of your Isabelle environment. The code inside the \isacommand{ML}-command can also contain value and function bindings, and even those can be - undone when the proof script is retracted. In what follows we will drop the - \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} whenever - we show code and its response. + undone when the proof script is retracted. For better readability, we will in what + follows drop the \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} + whenever we show code and its response. Once a portion of code is relatively stable, one usually wants to export it to a separate ML-file. Such files can then be included in a @@ -51,7 +52,7 @@ \begin{tabular}{@ {}l} \isacommand{theory} FirstSteps\\ \isacommand{imports} Main\\ - \isacommand{uses} @{ML_text "\"file_to_be_included.ML\""} @{text "\"}\\ + \isacommand{uses} @{text "\"file_to_be_included.ML\""} @{text "\"}\\ \isacommand{begin}\\ \ldots \end{tabular} @@ -67,14 +68,14 @@ in your code. This can be done in a ``quick-and-dirty'' fashion using the function @{ML "warning"}. For example - @{ML [display] "warning \"any string\""} + @{ML_response_fake [display] "warning \"any string\"" "\"any string\""} - will print out @{ML_text [quotes] "any string"} inside the response buffer - of Isabelle. This function expects a string. If you develop under PolyML, + will print out @{text [quotes] "any string"} inside the response buffer + of Isabelle. This function expects a string as argument. If you develop under PolyML, then there is a convenient, though again ``quick-and-dirty'', method for converting values into strings, for example: - @{ML [display] "warning (makestring 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. @@ -85,9 +86,9 @@ function @{ML tracing} is more appropriate. This function writes all output into a separate tracing buffer. For example - @{ML [display] "tracing \"foo\""} + @{ML_response_fake [display] "tracing \"foo\"" "\"foo\""} - It is also possible to redirect the ``channel'' where the string @{ML_text "foo"} is + It is also possible to redirect the ``channel'' where the string @{text "foo"} is printed to a separate file, e.g. to prevent Proof General from choking on massive amounts of trace output. This redirection can be achieved using the code *} @@ -110,7 +111,7 @@ text {* Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} - will cause that all tracing information is printed into the file @{ML_text "foo.bar"}. + will cause that all tracing information is printed into the file @{text "foo.bar"}. *} @@ -119,17 +120,17 @@ text {* The main advantage of embedding all code in a theory is that the code can - contain references to entities defined on the logical level of Isabelle (by - this we mean definitions, theorems, terms and so on). This is done using - antiquotations. For example, one can print out the name of the current + contain references to entities defined on the logical level of Isabelle. By + this we mean definitions, theorems, terms and so on. This kind of reference is + realised with antiquotations. For example, one can print out the name of the current theory by typing - @{ML_response [display] "Context.theory_name @{theory}" "FirstSteps"} + @{ML_response [display] "Context.theory_name @{theory}" "\"FirstSteps\""} where @{text "@{theory}"} is an antiquotation that is substituted with the current theory (remember that we assumed we are inside the theory - @{ML_text FirstSteps}). The name of this theory can be extracted using + @{text FirstSteps}). The name of this theory can be extracted with the function @{ML "Context.theory_name"}. Note, however, that antiquotations are statically scoped, that is the value is @@ -142,9 +143,9 @@ text {* - does \emph{not} return the name of the current theory, if it is run in a + does, as its name suggest, \emph{not} return the name of the current theory, if it is run in a different theory. Instead, the code above defines the constant function - that always returns the string @{ML_text "FirstSteps"}, no matter where the + that always returns the string @{text [quotes] "FirstSteps"}, no matter where the function is called. Operationally speaking, the antiquotation @{text "@{theory}"} is \emph{not} replaced with code that will look up the current theory in some data structure and return it. Instead, it is literally @@ -158,7 +159,7 @@ (FIXME: what does a simpset look like? It seems to be the same problem like tokens.) - While antiquotations have many applications, they were originally introduced to + While antiquotations nowadays have many applications, they were originally introduced to avoid explicit bindings for theorems such as *} @@ -167,11 +168,11 @@ *} text {* - These bindings were difficult to maintain and also could be accidentally - overwritten by the user. This usually broke definitional + These bindings were difficult to maintain and also could accidentally + be overwritten by the user. This usually broke definitional packages. Antiquotations solve this problem, since they are ``linked'' statically at compile-time. However, that also sometimes limits their - applicability. In the course of this introduction, we will learn more about + usefulness. In the course of this introduction, we will learn more about these antiquotations: they greatly simplify Isabelle programming since one can directly access all kinds of logical elements from ML. @@ -289,10 +290,10 @@ @{text "+"} are more complex than one first expects, namely \begin{center} - @{ML_text "HOL.zero_class.zero"} and @{ML_text "HOL.plus_class.plus"}. + @{text "HOL.zero_class.zero"} and @{text "HOL.plus_class.plus"}. \end{center} - The extra prefixes @{ML_text zero_class} and @{ML_text plus_class} are present because + The extra prefixes @{text zero_class} and @{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 Isabelle provides the antiquotation @{text "@{const_name \}"} which does the @@ -332,7 +333,7 @@ text {* \begin{exercise}\label{fun:revsum} - Write a function @{ML_text "rev_sum : term -> term"} that takes a + Write a function @{text "rev_sum : term -> term"} that takes a term of the form @{text "t\<^isub>1 + t\<^isub>2 + \ + t\<^isub>n"} (whereby @{text "i"} might be zero) and returns the reversed sum @{text "t\<^isub>n + \ + t\<^isub>2 + t\<^isub>1"}. Assume the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} diff -r 065f472c09ab -r f3794c231898 CookBook/Parsing.thy --- a/CookBook/Parsing.thy Tue Dec 16 17:37:39 2008 +0100 +++ b/CookBook/Parsing.thy Tue Dec 16 17:28:05 2008 +0000 @@ -46,20 +46,20 @@ @{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 exception - @{ML_text "FAIL"} if no string can be consumed. For example trying to parse + @{text "FAIL"} if no string can be consumed. For example trying to parse @{ML_response_fake [display] "($$ \"x\") (explode \"world\")" "Exception FAIL raised"} - will raise the exception @{ML_text "FAIL"}. + will raise the exception @{text "FAIL"}. There are three exceptions used in the parsing combinators: \begin{itemize} - \item @{ML_text "FAIL"} is used to indicate that alternative routes of parsing + \item @{text "FAIL"} is used to indicate that alternative routes of parsing might be explored. - \item @{ML_text "MORE"} indicates that there is not enough input for the parser. For example - in @{ML_text "($$ \"h\") []"}. - \item @{ML_text "ABORT"} is the exception which is raised when a dead end is reached. + \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. It is used for example in the function @{ML "(op !!)"} (see below). \end{itemize} @@ -69,7 +69,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 predicate. For example the - following parser either consumes an @{ML_text [quotes] "h"} or a @{ML_text + following parser either consumes an @{text [quotes] "h"} or a @{text [quotes] "w"}: @@ -84,7 +84,7 @@ "((\"h\", [\"e\", \"l\", \"l\", \"o\"]),(\"w\", [\"o\", \"r\", \"l\", \"d\"]))"} 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 + For example parsing @{text "h"}, @{text "e"} and @{text "l"} in this sequence can be achieved by @{ML_response [display] "(($$ \"h\") -- ($$ \"e\") -- ($$ \"l\")) (explode \"hello\")" @@ -100,8 +100,8 @@ Parsers that explore alternatives can be constructed using the function @{ML "(op ||)"}. For example, the parser @{ML "(p || q)" for p q} returns the - result of @{ML_text "p"}, in case it succeeds, otherwise it returns the - result of @{ML_text "q"}. For example + result of @{text "p"}, in case it succeeds, otherwise it returns the + result of @{text "q"}. For example @{ML_response [display] @@ -129,8 +129,8 @@ "((\"e\", [\"l\", \"l\", \"o\"]),(\"h\", [\"l\", \"l\", \"o\"]))"} The parser @{ML "Scan.optional p x" for p x} returns the result of the parser - @{ML_text "p"}, if it succeeds; otherwise it returns - the default value @{ML_text "x"}. For example + @{text "p"}, if it succeeds; otherwise it returns + the default value @{text "x"}. For example @{ML_response [display] "let @@ -155,8 +155,8 @@ end" "((SOME \"h\", [\"e\", \"l\", \"l\", \"o\"]), (NONE, [\"w\", \"o\", \"r\", \"l\", \"d\"]))"} The function @{ML "(op !!)"} helps to produce appropriate error messages - during parsing. For example if one wants to parse that @{ML_text p} is immediately - followed by @{ML_text q}, or start a completely different parser @{ML_text r}, + during parsing. For example if one wants to parse that @{text p} is immediately + followed by @{text q}, or start a completely different parser @{text r}, one might write @{ML [display] "(p -- q) || r" for p q r} @@ -164,31 +164,31 @@ However, this parser is problematic for producing an appropriate error message, in case the parsing of @{ML "(p -- q)" for p q} fails. Because in that case one loses with the parser above the information - that @{ML_text p} should be followed by @{ML_text q}. To see this consider the case in - which @{ML_text p} - is present in the input, but not @{ML_text q}. That means @{ML "(p -- q)" for p q} will fail + that @{text p} should be followed by @{text q}. To see this consider the case in + which @{text p} + is present in the input, but not @{text q}. That means @{ML "(p -- q)" for p q} will fail and the - alternative parser @{ML_text r} will be tried. However in many circumstance this will be the wrong + alternative parser @{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 absence of @{ML_text q} in the input. This kind of situation + failure of @{text r}, not by the absence of @{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\"))"} - on @{ML_text [quotes] "hello"}, the parsing succeeds + on @{text [quotes] "hello"}, the parsing succeeds @{ML_response [display] "(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"} - but if we invoke it on @{ML_text [quotes] "world"} + but if we invoke it on @{text [quotes] "world"} @{ML_response_fake [display] "(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"world\")" "Exception ABORT raised"} - the parsing aborts and the error message @{ML_text "foo"} is printed out. In order to + the parsing aborts and the error message @{text "foo"} is printed out. In order to see the error message properly, we need to prefix the parser with the function @{ML "Scan.error"}. For example @@ -226,18 +226,18 @@ yields the expected parsing. - The function @{ML "Scan.repeat p" for p} will apply a parser @{ML_text p} as + The function @{ML "Scan.repeat p" for p} will apply a parser @{text p} as often as it succeeds. For example @{ML_response [display] "Scan.repeat ($$ \"h\") (explode \"hhhhello\")" "([\"h\", \"h\", \"h\", \"h\"], [\"e\", \"l\", \"l\", \"o\"])"} Note that @{ML "Scan.repeat"} stores the parsed items in a list. The function - @{ML "Scan.repeat1"} is similar, but requires that the parser @{ML_text "p"} + @{ML "Scan.repeat1"} is similar, but requires that the parser @{text "p"} succeeds at least once. - Also note that the parser would have aborted with the exception @{ML_text MORE}, if - we had run it only on just @{ML_text [quotes] "hhhh"}. This can be avoided using + Also note that the parser would have aborted with the exception @{text MORE}, if + we had run it only on just @{text [quotes] "hhhh"}. This can be avoided using the wrapper @{ML Scan.finite} and the ``stopper-token'' @{ML Symbol.stopper}. With them we can write @@ -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] "*"}: + symbol is a @{text [quotes] "*"} which causes the parser to stop: @{ML_response [display] "let @@ -293,8 +293,8 @@ After parsing succeeded, one nearly always wants to apply a function on the parsed items. This is done using the function @{ML "(p >> f)" for p f} which runs - first the parser @{ML_text p} and upon successful completion applies the - function @{ML_text f} to the result. For example + first the parser @{text p} and upon successful completion applies the + function @{text f} to the result. For example @{ML_response [display] "let @@ -307,10 +307,11 @@ doubles the two parsed input strings. \begin{exercise}\label{ex:scancmts} - Write a parser parses an input string so that any comment enclosed inside - @{text "(*\*)"} is enclosed inside @{text "(**\**)"} in the output - string. To enclose a string, you can use the function @{ML "enclose s1 s2 s" - for s1 s2 s} which produces the string @{ML "s1^s^s2" for s1 s2 s}. + Write a parser that parses an input string so that any comment enclosed + inside @{text "(*\*)"} is replaced by a the same comment but enclosed inside + @{text "(**\**)"} in the output string. To enclose a string, you can use the + function @{ML "enclose s1 s2 s" for s1 s2 s} which produces the string @{ML + "s1^s^s2" for s1 s2 s}. \end{exercise} @@ -358,7 +359,7 @@ Token (\,(Ident, \"world\"),\)]"} produces three tokens where the first and the last are identifiers, since - @{ML_text [quotes] "hello"} and @{ML_text [quotes] "world"} do not match any + @{text [quotes] "hello"} and @{text [quotes] "world"} do not match any other syntactic category.\footnote{Note that because of a possible a bug in the PolyML runtime system the result is printed as @{text "?"}, instead of the token.} The second indicates a space. @@ -430,8 +431,8 @@ "((\"|\",\"in\"),[])"} The parser @{ML "OuterParse.enum s p" for s p} parses a possibly empty - list of items recognised by the parser @{ML_text p}, where the items being parsed - are separated by the string @{ML_text s}. For example + list of items recognised by the parser @{text p}, where the items being parsed + are separated by the string @{text s}. For example @{ML_response [display] "let @@ -442,9 +443,9 @@ "([\"in\",\"in\",\"in\"],[\])"} @{ML "OuterParse.enum1"} works similarly, except that the parsed list must - be non-empty. Note that we had to add an @{ML_text [quotes] "foo"} at the end + be non-empty. Note that we had to add an @{text [quotes] "foo"} at the end of the parsed string, otherwise the parser would have consumed all tokens - and then failed with the exception @{ML_text "MORE"}. Like in the previous + and then failed with the exception @{text "MORE"}. Like in the previous section, we can avoid this exception using the wrapper @{ML Scan.finite}. This time, however, we have to use the ``stopper-token'' @{ML OuterLex.stopper}. We can write diff -r 065f472c09ab -r f3794c231898 CookBook/Readme.thy --- a/CookBook/Readme.thy Tue Dec 16 17:37:39 2008 +0100 +++ b/CookBook/Readme.thy Tue Dec 16 17:28:05 2008 +0000 @@ -20,12 +20,12 @@ \begin{center} \begin{tabular}{l|c|c} & Chapters & Sections\\\hline - Implementation Manual & @{ML_text "\\ichcite{\}"} & @{ML_text "\\isccite{\}"}\\ - Isar Reference Manual & @{ML_text "\\rchcite{\}"} & @{ML_text "\\rsccite{\}"}\\ + Implementation Manual & @{text "\\ichcite{\}"} & @{text "\\isccite{\}"}\\ + Isar Reference Manual & @{text "\\rchcite{\}"} & @{text "\\rsccite{\}"}\\ \end{tabular} \end{center} - So @{ML_text "\\ichcite{ch:logic}"} yields a reference for the chapter about logic + So @{text "\\ichcite{ch:logic}"} yields a reference for the chapter about logic in the implementation manual, namely \ichcite{ch:logic}. \item There are various document antiquotations defined for the @@ -37,50 +37,99 @@ The following antiquotations are defined: \begin{itemize} - \item[$\bullet$] @{text "@{ML \"\\" for \ in \}"} should be used for - displaying any ML-ex\-pression, because it checks whether the expression is valid - ML-code. The @{text "for"} and @{text "in"} arguments are optional. The - former is used for evaluating open expressions by giving a list of - free variables. The latter is used to indicate in which structure or structures the - ML-expression should be evaluated. Examples are: + \item[$\bullet$] @{text "@{ML \"expr\" for vars in structs}"} should be used + for displaying any ML-ex\-pression, because the antiquotation checks whether + the expression is valid ML-code. The @{text "for"}- and @{text + "in"}-arguments are optional. The former is used for evaluating open + expressions by giving a list of free variables. The latter is used to + indicate in which structure or structures the ML-expression should be + evaluated. Examples are: \begin{center}\small + \begin{tabular}{lll} + @{text "@{ML \"1 + 3\"}"} & & @{ML "1 + 3"}\\ + @{text "@{ML \"a + b\" for a b}"} & produce & @{ML "a + b" for a b}\\ + @{text "@{ML Ident in OuterLex}"} & & @{ML Ident in OuterLex}\\ + \end{tabular} + \end{center} + + \item[$\bullet$] @{text "@{ML_response \"expr\" \"pat\"}"} should be used to + display ML-expressions and their response. The first expression is checked + like in the antiquotation @{text "@{ML \"expr\"}"}; the second is a pattern + that specifies the result the first expression produces. This pattern can + contain @{text "\"} for parts that you like to omit. The response of the + first expression will be checked against this pattern. Examples are: + + \begin{center}\small \begin{tabular}{l} - @{text "@{ML \"1 + 3\"}"}\\ - @{text "@{ML \"a + b\" for a b}"}\\ - @{text "@{ML Ident in OuterLex}"} + @{text "@{ML_response \"1+2\" \"3\"}"}\\ + @{text "@{ML_response \"(1+2,3)\" \"(3,\)\"}"} \end{tabular} \end{center} - \item[$\bullet$] @{text "@{ML_response \"\\" \"\\"}"} should be used to - display ML-ex\-pressions and their response. - The first expression is checked like in the antiquotation @{text "@{ML \"\\"}"}; the - second is a pattern that specifies the result the first expression - produces. This specification can contain @{text "\"} for parts that - you like to omit. The response of the first expresion will be checked against - this specification. An example is @{text "@{ML_response \"(1+2,3)\" - \"(3,\)\"}"}. This antiquotation can only be used when the result can be + which produce respectively + + \begin{center}\small + \begin{tabular}{p{3cm}p{3cm}} + @{ML_response "1+2" "3"} & + @{ML_response "(1+2,3)" "(3,\)"} + \end{tabular} + \end{center} + + Note that this antiquotation can only be used when the result can be constructed: it does not work when the code produces an exception or returns an abstract datatype (like @{ML_type thm} or @{ML_type cterm}). - \item[$\bullet$] @{text "@{ML_response_fake \"\\" \"\\"}"} Works like - the @{ML_text ML_response}-anti\-quotation, except that the - result-specification is not checked. Use this antiquotation - if the result cannot be constructed or the code generates an exception. + \item[$\bullet$] @{text "@{ML_response_fake \"expr\" \"pat\"}"} works just + like the antiquotation @{text "@{ML_response \"expr\" \"pat\"}"} above, + except that the result-specification is not checked. Use this antiquotation + when the result cannot be constructed or the code generates an + exception. Examples are: + + \begin{center}\small + \begin{tabular}{ll} + @{text "@{ML_response"} & @{text "\"cterm_of @{theory} @{term \\\"a + b = c\\\"}\"}"}\\ + & @{text "\"a + b = c\"}"}\smallskip\\ + @{text "@{ML_response"} & @{text "\"($$ \\\"x\\\") (explode \\\"world\\\")\""}\\ + & @{text "\"Exception FAIL raised\"}"} + \end{tabular} + \end{center} + - \item[$\bullet$] @{text "@{ML_response_fake_both \"\\" \"\\"}"} can be + \item[$\bullet$] @{text "@{ML_response_fake_both \"expr\" \"pat\"}"} can be used to show erroneous code. Neither the code nor the response will be - chacked. + checked. An example is: - \item[$\bullet$] @{text "@{ML_file \"\\"}"} Should be used when + \begin{center}\small + \begin{tabular}{ll} + @{text "@{ML_response_fake_both"} & @{text "\"@{cterm \\\"1 + True\\\"}\""}\\ + & @{text "\"Type unification failed \\"}"} + \end{tabular} + \end{center} + + \item[$\bullet$] @{text "@{ML_file \"name\"}"} should be used when referring to a file. It checks whether the file exists. \end{itemize} + The listed antiquotations honour options including @{text "[display]"} and + @{text "[quotes]"}. For example + + \begin{center}\small + @{text "@{ML [quotes] \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces\;\; @{text [quotes] "foobar"} + \end{center} + + while + + \begin{center}\small + @{text "@{ML \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces only\;\; @{text "foobar"} + \end{center} + + \item Functions and value bindings cannot be defined inside antiquotations; they need to be included inside \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} - environments. In this way they are also checked by the compiler. Some \LaTeX-hack, however, - ensures that the environment markers are not printed. + environments. In this way they are also checked by the compiler. Some \LaTeX-hack in + the Cookbook, however, ensures that the environment markers are not printed. \item Line numbers can be printed using \isacommand{ML} \isa{\%linenumbers} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} diff -r 065f472c09ab -r f3794c231898 CookBook/Recipes/Antiquotes.thy --- a/CookBook/Recipes/Antiquotes.thy Tue Dec 16 17:37:39 2008 +0100 +++ b/CookBook/Recipes/Antiquotes.thy Tue Dec 16 17:28:05 2008 +0000 @@ -21,12 +21,12 @@ provides a sanity check for the code and also allows one to keep documents in sync with other code, for example Isabelle. - We first describe the antiquotation @{text "@{ML_checked \"\\"}"}. This - antiquotation takes a piece of code as argument; this code is then checked + We first describe the antiquotation @{text "@{ML_checked \"expr\"}"}. This + antiquotation takes a piece of code as argument. The argument is checked by sending the ML-expression @{text [quotes] "val _ = \"} containing the - given code to the ML-compiler (i.e.~the function @{ML "ML_Context.eval_in"} - in the snippet below). The code for @{text "@{ML_checked \"\\"}"} is as - follows: + given argument to the ML-compiler (i.e.~the function @{ML "ML_Context.eval_in"} + in Line 4 in the code below). The code of @{text "@{ML_checked \"expr\"}"} + is as follows: *} @@ -44,12 +44,12 @@ text {* Note that the parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, - in this case the code. This code is send to the ML-compiler in the line 4. + in this case the code given as argument. This argument is send to the ML-compiler in the line 4. If the code is ``approved'' by the compiler, then the output function @{ML "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"} in the next line pretty prints the code. This function expects that the code is a list of strings where each - string correspond to a line (therefore the @{ML "(space_explode \"\\n\" txt)" for txt} - which produces this list). There are a number of options for antiquotations + string correspond to a line. Therefore the @{ML "(space_explode \"\\n\" txt)" for txt} + which produces this list. There are a number of options for antiquotations that are observed by @{ML ThyOutput.output_list} when printing the code (for example @{text "[display]"}, @{text "[quotes]"} and @{text "[source]"}). @@ -63,8 +63,7 @@ *} -ML {* -fun output_ml ml src ctxt (txt,pos) = +ML %linenumbers {* fun output_ml ml src ctxt (txt,pos) = (ML_Context.eval_in (SOME ctxt) false pos (ml txt); ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt)) @@ -75,35 +74,40 @@ *} text {* + where in Lines 1 and 2 the positional information is properly treated. + (FIXME: say something about OuterParse.position) We can now write in a document @{text "@{ML_checked \"2 + 3\"}"} in order to obtain @{ML_checked "2 + 3"} and be sure that this code compiles until - somebody changes the definition of @{ML "(op +)"}. + somebody changes the definition of \mbox{@{ML "(op +)"}}. - The second antiquotation extends the first by allowing to also give - hints what the result of the ML-code is and check consistency of these - hints. For this we use the antiquotation @{text "@{ML_response \"\\" \"\\"}"} - whose first argument is the ML-code and the second is the result. + The second antiquotation extends the first by allowing also to give + hints what the result of the ML-code is and check the consistency of + the actual result with these hints. For this we use the antiquotation + @{text "@{ML_response \"expr\" \"pat\"}"} + whose first argument is the ML-code and the second is a pattern specifying + the result. To add some convenience we allow the user to give a partial + specification using @{text "\"}. - In the antiquotation @{text "@{ML_checked \"\\"}"} we send the expresion - @{text [quotes] "val _ = \"} to the compiler. Now we will use the hints - to construct a pattern for the @{text "_"}. To add some convenince we allow - the user to give partial hints using @{text "\"}, which however need to - be replaced by @{text "_"} before sending the code to the compiler. The - function + In the antiquotation @{text "@{ML_checked \"expr\"}"} we send the expression + @{text [quotes] "val _ = expr"} to the compiler. Instead of the wildcard + @{text "_"}, we will here use the hints to construct a proper pattern. To + do this we need to replace the @{text "\"} by @{text "_"} before sending the + code to the compiler. The function *} -ML {* +ML {* fun ml_pat (rhs, pat) = let val pat' = implode (map (fn "\" => "_" | s => s) (Symbol.explode pat)) in "val " ^ pat' ^ " = " ^ rhs end; *} text {* - will do this. Next we like to add a response indicator to the result using: + will construct the pattern that the compiler can use. Next we like to add + a response indicator to the result using: *} @@ -152,7 +156,6 @@ *} - end diff -r 065f472c09ab -r f3794c231898 CookBook/Recipes/NamedThms.thy --- a/CookBook/Recipes/NamedThms.thy Tue Dec 16 17:37:39 2008 +0100 +++ b/CookBook/Recipes/NamedThms.thy Tue Dec 16 17:28:05 2008 +0000 @@ -1,5 +1,5 @@ theory NamedThms -imports Base +imports "../Base" begin section {* Accumulate a List of Theorems under a Name *} @@ -27,16 +27,16 @@ text {* and the command - @{ML_text [display] "setup FooRules.setup"} + @{text [display] "setup FooRules.setup"} This code declares a context data slot where the theorems are stored, - an attribute @{ML_text foo} (with the usual @{ML_text add} and @{ML_text del} options + an attribute @{text foo} (with the usual @{text add} and @{text del} options for adding and deleting theorems) and an internal ML interface to retrieve and modify the theorems. Furthermore, the facts are made available on the user level under the dynamic fact name @{text foo}. For example we can declare three lemmas to be of the kind - @{ML_text foo} by: + @{text foo} by: *} lemma rule1[foo]: "A" sorry @@ -52,7 +52,7 @@ thm foo text {* - On the ML-level the rules marked with @{ML_text "foo"} an be retrieved + On the ML-level the rules marked with @{text "foo"} an be retrieved using the function @{ML FooRules.get}: @{ML_response_fake [display] "FooRules.get @{context}" "[\"?C\",\"?B\"]"} diff -r 065f472c09ab -r f3794c231898 CookBook/Solutions.thy --- a/CookBook/Solutions.thy Tue Dec 16 17:37:39 2008 +0100 +++ b/CookBook/Solutions.thy Tue Dec 16 17:28:05 2008 +0000 @@ -34,7 +34,7 @@ val end_cmt = Scan.this_string "*)" in begin_cmt |-- Scan.repeat (Scan.unless end_cmt any) --| end_cmt - >> (enclose "(**" "**)" o implode) + >> (enclose "(**" "**)" o implode) end val scan_all = @@ -43,8 +43,9 @@ *} text {* - By using @{ML_text "#> fst"} in the last line, the function - @{ML scan_all} retruns a string instead of a pair. For example: + By using @{text "#> fst"} in the last line, the function + @{ML scan_all} retruns a string, instead of the pair a parser would + normally return. For example: @{ML_response [display] "scan_all (explode \"foo bar\")" "\"foo bar\""} diff -r 065f472c09ab -r f3794c231898 cookbook.pdf Binary file cookbook.pdf has changed