--- a/CookBook/Package/Ind_Interface.thy	Fri Nov 28 05:56:28 2008 +0100
+++ b/CookBook/Package/Ind_Interface.thy	Sat Nov 29 21:20:18 2008 +0000
@@ -27,9 +27,13 @@
 handling strings that are lacking the additional structure of terms. These two ways of
 invoking the package are reflected in its ML programming interface, which consists of two
 functions:
+
 @{ML_chunk [display] SIMPLE_INDUCTIVE_PACKAGE}
-The function for external invocation of the package is called @{ML_open add_inductive (SIP)},
-whereas the one for internal invocation is called @{ML_open add_inductive_i (SIP)}. Both
+*}
+
+text {*
+The function for external invocation of the package is called @{ML add_inductive in SIP},
+whereas the one for internal invocation is called @{ML add_inductive_i in SIP}. Both
 of these functions take as arguments the names and types of the inductive predicates, the
 names and types of their parameters, the actual introduction rules and a \emph{local theory}.
 They return a local theory containing the definition, together with a tuple containing
@@ -40,13 +44,13 @@
 that may be used by the package. The type @{ML_type local_theory} is identical to the
 type of \emph{proof contexts} @{ML_type "Proof.context"}, although not every proof context
 constitutes a valid local theory.
-Note that @{ML_open add_inductive_i (SIP)} expects the types
+Note that @{ML add_inductive_i in SIP} expects the types
 of the predicates and parameters to be specified using the datatype @{ML_type typ} of Isabelle's
-logical framework, whereas @{ML_open add_inductive (SIP)}
+logical framework, whereas @{ML add_inductive in SIP}
 expects them to be given as optional strings. If no string is
 given for a particular predicate or parameter, this means that the type should be
 inferred by the package. Additional \emph{mixfix syntax} may be associated with
-the predicates and parameters as well. Note that @{ML_open add_inductive_i (SIP)} does not
+the predicates and parameters as well. Note that @{ML add_inductive_i in SIP} does not
 allow mixfix syntax to be associated with parameters, since it can only be used
 for parsing. The names of the predicates, parameters and rules are represented by the
 type @{ML_type Name.binding}. Strings can be turned into elements of the type
@@ -55,45 +59,51 @@
 Each introduction rule is given as a tuple containing its name, a list of \emph{attributes}
 and a logical formula. Note that the type @{ML_type Attrib.binding} used in the list of
 introduction rules is just a shorthand for the type @{ML_type "Name.binding * Attrib.src list"}.
-The function @{ML_open add_inductive_i (SIP)} expects the formula to be specified using the datatype
-@{ML_type term}, whereas @{ML_open add_inductive (SIP)} expects it to be given as a string.
+The function @{ML add_inductive_i in SIP} expects the formula to be specified using the datatype
+@{ML_type term}, whereas @{ML add_inductive in SIP} expects it to be given as a string.
 An attribute specifies additional actions and transformations that should be applied to
 a theorem, such as storing it in the rule databases used by automatic tactics
 like the simplifier. The code of the package, which will be described in the following
 section, will mostly treat attributes as a black box and just forward them to other
 functions for storing theorems in local theories.
-The implementation of the function @{ML_open add_inductive (SIP)} for external invocation
+The implementation of the function @{ML add_inductive in SIP} for external invocation
 of the package is quite simple. Essentially, it just parses the introduction rules
-and then passes them on to @{ML_open add_inductive_i (SIP)}:
+and then passes them on to @{ML add_inductive_i in SIP}:
 @{ML_chunk [display] add_inductive}
 For parsing and type checking the introduction rules, we use the function
-@{ML_open [display] "Specification.read_specification:
+@{ML [display] "Specification.read_specification:
   (Name.binding * string option * mixfix) list ->  (*{variables}*)
   (Attrib.binding * string list) list list ->  (*{rules}*)
   local_theory ->
   (((Name.binding * typ) * mixfix) list *
    (Attrib.binding * term list) list) *
   local_theory"}
+*}
+
+text {*
 During parsing, both predicates and parameters are treated as variables, so
 the lists \verb!preds_syn! and \verb!params_syn! are just appended
-before being passed to @{ML_open read_specification (Specification)}. Note that the format
-for rules supported by @{ML_open read_specification (Specification)} is more general than
+before being passed to @{ML read_specification in Specification}. Note that the format
+for rules supported by @{ML read_specification in Specification} is more general than
 what is required for our package. It allows several rules to be associated
 with one name, and the list of rules can be partitioned into several
 sublists. In order for the list \verb!intro_srcs! of introduction rules
-to be acceptable as an input for @{ML_open read_specification (Specification)}, we first
+to be acceptable as an input for @{ML read_specification in Specification}, we first
 have to turn it into a list of singleton lists. This transformation
 has to be reversed later on by applying the function
 @{ML [display] "the_single: 'a list -> 'a"}
 to the list \verb!specs! containing the parsed introduction rules.
-The function @{ML_open read_specification (Specification)} also returns the list \verb!vars!
+The function @{ML read_specification in Specification} also returns the list \verb!vars!
 of predicates and parameters that contains the inferred types as well.
 This list has to be chopped into the two lists \verb!preds_syn'! and
 \verb!params_syn'! for predicates and parameters, respectively.
 All variables occurring in a rule but not in the list of variables passed to
-@{ML_open read_specification (Specification)} will be bound by a meta-level universal
+@{ML read_specification in Specification} will be bound by a meta-level universal
 quantifier.
-Finally, @{ML_open read_specification (Specification)} also returns another local theory,
+*}
+
+text {*
+Finally, @{ML read_specification in Specification} also returns another local theory,
 but we can safely discard it. As an example, let us look at how we can use this
 function to parse the introduction rules of the @{text trcl} predicate:
 @{ML_response [display]
@@ -119,17 +129,19 @@
  \<dots>)
 : (((Name.binding * typ) * mixfix) list *
    (Attrib.binding * term list) list) * local_theory"}
-In the list of variables passed to @{ML_open read_specification (Specification)}, we have
+In the list of variables passed to @{ML read_specification in Specification}, we have
 used the mixfix annotation @{ML NoSyn} to indicate that we do not want to associate any
 mixfix syntax with the variable. Moreover, we have only specified the type of \texttt{r},
 whereas the type of \texttt{trcl} is computed using type inference.
 The local variables \texttt{x}, \texttt{y} and \texttt{z} of the introduction rules
 are turned into bound variables with the de Bruijn indices,
 whereas \texttt{trcl} and \texttt{r} remain free variables.
+*}
 
+text {*
 \paragraph{Parsers for theory syntax}
 
-Although the function @{ML_open add_inductive (SIP)} parses terms and types, it still
+Although the function @{ML add_inductive in SIP} parses terms and types, it still
 cannot be used to invoke the package directly from within a theory document.
 In order to do this, we have to write another parser. Before we describe
 the process of writing parsers for theory syntax in more detail, we first
@@ -294,38 +306,38 @@
 @{ML "-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e"} \\
 @{ML "|-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e"} \\
 @{ML "--| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e"} \\
-@{ML_open "optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a" (Scan)} \\
-@{ML_open "repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a" (Scan)} \\
-@{ML_open "repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a" (Scan)} \\
+@{ML "optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a" in Scan} \\
+@{ML "repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a" in Scan} \\
+@{ML "repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a" in Scan} \\
 @{ML ">> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c"} \\
 @{ML "!! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b"}
 \end{mytable}
 Interestingly, the functions shown above are so generic that they do not
 even rely on the input and output of the parser being a list of tokens.
 If \texttt{p} succeeds, i.e.\ does not raise an exception, the parser
-@{ML_open "p || q" for p q} returns the result of \texttt{p}, otherwise it returns
-the result of \texttt{q}. The parser @{ML_open "p -- q" for p q} first parses an
+@{ML "p || q" for p q} returns the result of \texttt{p}, otherwise it returns
+the result of \texttt{q}. The parser @{ML "p -- q" for p q} first parses an
 item of type @{ML_type "'b"} using \texttt{p}, then passes the remaining tokens
 of type @{ML_type "'c"} to \texttt{q}, which parses an item of type @{ML_type "'d"}
 and returns the remaining tokens of type @{ML_type "'e"}, which are finally
 returned together with a pair of type @{ML_type "'b * 'd"} containing the two
-parsed items. The parsers @{ML_open "p |-- q" for p q} and @{ML_open "p --| q" for p q}
+parsed items. The parsers @{ML "p |-- q" for p q} and @{ML "p --| q" for p q}
 work in a similar way as the previous one, with the difference that they
 discard the item parsed by the first and the second parser, respectively.
-If \texttt{p} succeeds, the parser @{ML_open "optional p x" for p x (Scan)} returns the result
+If \texttt{p} succeeds, the parser @{ML "optional p x" for p x in Scan} returns the result
 of \texttt{p}, otherwise it returns the default value \texttt{x}. The parser
-@{ML_open "repeat p" for p (Scan)} applies \texttt{p} as often as it can, returning a possibly
-empty list of parsed items. The parser @{ML_open "repeat1 p" for p (Scan)} is similar,
+@{ML "repeat p" for p in Scan} applies \texttt{p} as often as it can, returning a possibly
+empty list of parsed items. The parser @{ML "repeat1 p" for p in Scan} is similar,
 but requires \texttt{p} to succeed at least once. The parser
-@{ML_open "p >> f" for p f} uses \texttt{p} to parse an item of type @{ML_type "'b"}, to which
+@{ML "p >> f" for p f} uses \texttt{p} to parse an item of type @{ML_type "'b"}, to which
 it applies the function \texttt{f} yielding a value of type @{ML_type "'d"}, which
 is returned together with the remaining tokens of type @{ML_type "'c"}.
 Finally, @{ML "!!"} is used for transforming exceptions produced by parsers.
 If \texttt{p} raises an exception indicating that it cannot parse a given input,
 then an enclosing parser such as
-@{ML_open [display] "q -- p || r" for p q r}
+@{ML [display] "q -- p || r" for p q r}
 will try the alternative parser \texttt{r}. By writing
-@{ML_open [display] "q -- !! err p || r" for err p q r}
+@{ML [display] "q -- !! err p || r" for err p q r}
 instead, one can achieve that a failure of \texttt{p} causes the whole parser to abort.
 The @{ML "!!"} operator is similar to the \emph{cut} operator in Prolog, which prevents
 the interpreter from backtracking. The \texttt{err} function supplied as an argument
@@ -337,14 +349,14 @@
 some basic parsers. As an example, we consider the following two parsers
 defined in @{ML_struct Scan}:
 \begin{mytable}
-@{ML_open "one: ('a -> bool) -> 'a list -> 'a * 'a list" (Scan)} \\
-@{ML_open "$$ : string -> string list -> string * string list"}
+@{ML "one: ('a -> bool) -> 'a list -> 'a * 'a list" in Scan} \\
+@{ML "$$ : string -> string list -> string * string list"}
 \end{mytable}
-The parser @{ML_open "one pred" for pred (Scan)} parses exactly one token that
-satisfies the predicate \texttt{pred}, whereas @{ML_open "$$ s" for s} only
+The parser @{ML "one pred" for pred in Scan} parses exactly one token that
+satisfies the predicate \texttt{pred}, whereas @{ML "$$ s" for s} only
 accepts a token that equals the string \texttt{s}. Note that we can easily
-express @{ML_open "$$ s" for s} using @{ML_open "one" (Scan)}:
-@{ML_open [display] "one (fn s' => s' = s)" for s (Scan)}
+express @{ML "$$ s" for s} using @{ML "one" in Scan}:
+@{ML [display] "one (fn s' => s' = s)" for s in Scan}
 As an example, let us look at how we can use @{ML "$$"} and @{ML "--"} to parse
 the prefix ``\texttt{hello}'' of the character list ``\texttt{hello world}'':
 @{ML_response [display]
@@ -360,37 +372,37 @@
 @{ML_struct OuterParse} defined in the file @{ML_file "Pure/Isar/outer_parse.ML"}.
 In our parser, we will use the following functions:
 \begin{mytable}
-@{ML_open "$$$ : string -> token list -> string * token list" (OuterParse)} \\
-@{ML_open "enum1: string -> (token list -> 'a * token list) -> token list ->
-  'a list * token list" (OuterParse)} \\
-@{ML_open "prop: token list -> string * token list" (OuterParse)} \\
-@{ML_open "opt_target: token list -> string option * token list" (OuterParse)} \\
-@{ML_open "fixes: token list ->
-  (Name.binding * string option * mixfix) list * token list" (OuterParse)} \\
-@{ML_open "for_fixes: token list ->
-  (Name.binding * string option * mixfix) list * token list" (OuterParse)} \\
-@{ML_open "!!! : (token list -> 'a) -> token list -> 'a" (OuterParse)}
+@{ML "$$$ : string -> token list -> string * token list" in OuterParse} \\
+@{ML "enum1: string -> (token list -> 'a * token list) -> token list ->
+  'a list * token list" in OuterParse} \\
+@{ML "prop: token list -> string * token list" in OuterParse} \\
+@{ML "opt_target: token list -> string option * token list" in OuterParse} \\
+@{ML "fixes: token list ->
+  (Name.binding * string option * mixfix) list * token list" in OuterParse} \\
+@{ML "for_fixes: token list ->
+  (Name.binding * string option * mixfix) list * token list" in OuterParse} \\
+@{ML "!!! : (token list -> 'a) -> token list -> 'a" in OuterParse}
 \end{mytable}
-The parsers @{ML_open "$$$" (OuterParse)} and @{ML_open "!!!" (OuterParse)} are
-defined using the parsers @{ML_open "one" (Scan)} and @{ML "!!"} from
+The parsers @{ML "$$$" in OuterParse} and @{ML "!!!" in OuterParse} are
+defined using the parsers @{ML "one" in Scan} and @{ML "!!"} from
 @{ML_struct Scan}.
-The parser @{ML_open "enum1 s p" for s p (OuterParse)} parses a non-emtpy list of items
+The parser @{ML "enum1 s p" for s p in OuterParse} parses a non-emtpy list of items
 recognized by the parser \texttt{p}, where the items are separated by \texttt{s}.
-A proposition can be parsed using the function @{ML_open prop (OuterParse)}.
+A proposition can be parsed using the function @{ML prop in OuterParse}.
 Essentially, a proposition is just a string or an identifier, but using the
-specific parser function @{ML_open prop (OuterParse)} leads to more instructive
+specific parser function @{ML prop in OuterParse} leads to more instructive
 error messages, since the parser will complain that a proposition was expected
 when something else than a string or identifier is found.
 An optional locale target specification of the form \isa{(\isacommand{in}\ $\ldots$)}
-can be parsed using @{ML_open opt_target (OuterParse)}.
+can be parsed using @{ML opt_target in OuterParse}.
 The lists of names of the predicates and parameters, together with optional
-types and syntax, are parsed using the functions @{ML_open "fixes" (OuterParse)}
-and @{ML_open for_fixes (OuterParse)}, respectively.
+types and syntax, are parsed using the functions @{ML "fixes" in OuterParse}
+and @{ML for_fixes in OuterParse}, respectively.
 In addition, the following function from @{ML_struct SpecParse} for parsing
 an optional theorem name and attribute, followed by a delimiter, will be useful:
 \begin{mytable}
-@{ML_open "opt_thm_name:
-  string -> token list -> Attrib.binding * token list" (SpecParse)}
+@{ML "opt_thm_name:
+  string -> token list -> Attrib.binding * token list" in SpecParse}
 \end{mytable}
 We now have all the necessary tools to write the parser for our
 \isa{\isacommand{simple{\isacharunderscore}inductive}} command:
@@ -399,9 +411,9 @@
 diagram shown above. In order to make the code more readable, the structures
 @{ML_struct OuterParse} and @{ML_struct OuterKeyword} are abbreviated by
 \texttt{P} and \texttt{K}, respectively. Note how the parser combinator
-@{ML_open "!!!" (OuterParse)} is used: once the keyword \texttt{where}
+@{ML "!!!" in OuterParse} is used: once the keyword \texttt{where}
 has been parsed, a non-empty list of introduction rules must follow.
-Had we not used the combinator @{ML_open "!!!" (OuterParse)}, a
+Had we not used the combinator @{ML "!!!" in OuterParse}, a
 \texttt{where} not followed by a list of rules would have caused the parser
 to respond with the somewhat misleading error message
 \begin{verbatim}
@@ -412,7 +424,7 @@
   Outer syntax error: proposition expected, but terminator was found
 \end{verbatim}
 Once all arguments of the command have been parsed, we apply the function
-@{ML_open add_inductive (SimpleInductivePackage)}, which yields a local theory
+@{ML add_inductive in SimpleInductivePackage}, which yields a local theory
 transformer of type @{ML_type "local_theory -> local_theory"}. Commands in
 Isabelle/Isar are realized by transition transformers of type
 @{ML_type [display] "Toplevel.transition -> Toplevel.transition"}
@@ -434,10 +446,10 @@
 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,
 we choose the kind @{ML "OuterKeyword.thy_decl"}. Other kinds include
-@{ML "OuterKeyword.thy_goal"}, which is similar to @{ML_open thy_decl (OuterKeyword)},
+@{ML "OuterKeyword.thy_goal"}, which is similar to @{ML thy_decl in OuterKeyword},
 but requires the user to prove a goal before making the declaration, or
 @{ML "OuterKeyword.diag"}, which corresponds to a purely diagnostic command that does
-not change the context. For example, the @{ML_open thy_goal (OuterKeyword)} kind is used
+not change the context. For example, the @{ML thy_goal in OuterKeyword} kind is used
 by the \isa{\isacommand{function}} command \cite{Krauss-IJCAR06}, which requires the user
 to prove that a given set of equations is non-overlapping and covers all cases. The kind
 of the command should be chosen with care, since selecting the wrong one can cause strange

--- a/CookBook/Parsing.thy	Fri Nov 28 05:56:28 2008 +0100
+++ b/CookBook/Parsing.thy	Sat Nov 29 21:20:18 2008 +0000
@@ -94,7 +94,7 @@
 
   Parsers that explore 
   alternatives can be constructed using the function @{ML "(op ||)"}. For example, the 
-  parser @{ML_open "(p || q)" for p q} returns the result of @{ML_text "p"}, in case it succeeds, 
+  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
 
 @{ML_response [display] 
@@ -121,7 +121,7 @@
 end"
   "((\"e\", [\"l\", \"l\", \"o\"]),(\"h\", [\"l\", \"l\", \"o\"]))"}
 
-  The parser @{ML_open "Scan.optional p x" for p x} returns the result of the parser 
+  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
 
@@ -152,14 +152,14 @@
   followed by @{ML_text q}, or start a completely different parser @{ML_text r},
   one might write
 
-  @{ML_open [display] "(p -- q) || r" for p q r}
+  @{ML [display] "(p -- q) || r" for p q r}
 
   However, this parser is problematic for producing an appropriate error message, in case
-  the parsing of @{ML_open "(p -- q)" for p q} fails. Because in that case one loses with the parser
+  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_open "(p -- q)" for p q} will fail 
+  is present in the input, but not @{ML_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
   parser for the input ``p-followed-by-q'' and therefore will also fail. The error message is then 
@@ -191,7 +191,7 @@
   This ``prefixing'' is usually done by wrappers such as @{ML "OuterSyntax.command"} 
   (FIXME: give reference to later place). 
   
-  Returning to our example of parsing @{ML_open "(p -- q) || r" for p q r}. If we want
+  Returning to our example of parsing @{ML "(p -- q) || r" for p q r}. If we want
   to generate the correct error message for p-followed-by-q, then
   we have to write:
 *}
@@ -219,7 +219,7 @@
   
   yields the expected parsing. 
 
-  The function @{ML_open "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 @{ML_text p} as 
   often as it succeeds. For example
   
   @{ML_response [display] "Scan.repeat ($$ \"h\") (explode \"hhhhello\")" 
@@ -241,7 +241,7 @@
   in practise, because it is already done by the infrastructure for you. 
 
   After parsing succeeded, one nearly always wants to apply a function on the parsed 
-  items. This is done using the function @{ML_open "(p >> f)" for p f} which runs 
+  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
 
@@ -281,14 +281,17 @@
   \end{readmore}
 
   The structure @{ML_struct OuterLex} defines several kinds of token (for example 
-  @{ML "OuterLex.Ident"} for identifiers, @{ML "OuterLex.Keyword"} for keywords and
-  @{ML "OuterLex.Command"} for commands). Some token parsers take into account the 
+  @{ML "Ident" in OuterLex} for identifiers, @{ML "Keyword" in OuterLex} for keywords and
+  @{ML "Command" in OuterLex} for commands). Some token parsers take into account the 
   kind of token.
-  
-  We can generate a token list out of a string using the function @{ML
-  "OuterSyntax.scan"}, which we give below @{ML "Position.none"} as argument
-  since, at the moment, we are not interested in generating precise error
-  messages. The following
+*}  
+
+text {*
+  For the examples below, we can generate a token list out of a string using
+  the function @{ML "OuterSyntax.scan"}, which we give below @{ML
+  "Position.none"} as argument since, at the moment, we are not interested in
+  generating precise error messages. The following
+
 
 @{ML_response_fake [display] "OuterSyntax.scan Position.none \"hello world\"" 
 "[Token (\<dots>,(Ident, \"hello\"),\<dots>), 
@@ -302,7 +305,7 @@
   the token.} The second indicates a space.
 
   Many parsing functions later on will require spaces, comments and the like
-  to have been filtered out.  In what follows below, we are going to use the 
+  to have already been filtered out.  So from now on we are going to use the 
   functions @{ML filter} and @{ML OuterLex.is_proper} do this. For example
 
 
@@ -367,20 +370,20 @@
 end"
 "((\"|\",\"in\"),[])"}
 
-  The parser @{ML_open "OuterParse.enum s p" for s p} parses a possibly empty 
-  list of items recognised by the parser @{ML_text p}, where the items are 
-  separated by the string @{ML_text s}. For example
+  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
 
 @{ML_response [display]
 "let 
-  val input = filtered_input \"in | in | in end\"
+  val input = filtered_input \"in | in | in foo\"
 in 
   (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input
 end" 
 "([\"in\",\"in\",\"in\"],[\<dots>])"}
 
   @{ML "OuterParse.enum1"} works similarly, except that the parsed list must
-  be non-empty. Note that we had to add a @{ML_text [quotes] "end"} at the end
+  be non-empty. Note that we had to add an @{ML_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
   section, we can avoid this exception using the wrapper @{ML
@@ -391,10 +394,21 @@
 "let 
   val input = filtered_input \"in | in | in\"
 in 
-  Scan.finite OuterLex.stopper (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input
+  Scan.finite OuterLex.stopper 
+         (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input
 end" 
 "([\"in\",\"in\",\"in\"],[])"}
 
+  The following function will help us to run examples
+
+*}
+
+ML {*
+fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input
+*}
+
+text {*
+
   The function @{ML "OuterParse.!!!"} can be used to force termination of the
   parser in case of a dead end, just like @{ML "Scan.!!"} (see previous section), 
   except that the error message is fixed to be @{text [quotes] "Outer syntax error"}
@@ -405,14 +419,22 @@
   val input = filtered_input \"in |\"
   val parse_bar_then_in = OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\"
 in 
-  Scan.error (OuterParse.!!! parse_bar_then_in) input 
+  parse (OuterParse.!!! parse_bar_then_in) input 
 end"
 "Exception ERROR \"Outer syntax error: keyword \"|\" expected, 
 but keyword in was found\" raised"
 }
 
+  \begin{exercise}
+  A type-identifier, for example @{typ "'a"}, is a token of 
+  kind @{ML "Keyword" in OuterLex} can be parsed 
+
+  \end{exercise}
+
+
 *}
 
+
 section {* Positional Information *}
 
 text {*

--- a/CookBook/Readme.thy	Fri Nov 28 05:56:28 2008 +0100
+++ b/CookBook/Readme.thy	Sat Nov 29 21:20:18 2008 +0000
@@ -2,11 +2,17 @@
 imports Base
 begin
 
-chapter {* Comments for Authors of the Cookbook *}
+chapter {* Comments for Authors *}
 
 text {*
 
   \begin{itemize}
+  \item The cookbook can be compiled on the command-line with:
+
+  \begin{center}
+  @{text "isabelle make"}
+  \end{center}
+
   \item You can include references to other Isabelle manuals using the 
   reference names from those manuals. To do this the following
   four latex commands are defined:
@@ -19,53 +25,62 @@
   \end{tabular}
   \end{center}
 
-  So @{ML_text "\\ichcite{ch:logic}"} results in a reference for the chapter about logic 
+  So @{ML_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 
-  cookbook. This allows to check the written text against the current
-  Isabelle code and also that responses of the ML-compiler can be shown.
+  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
-  it is appropriate.
+  appropriate.
   
-  The following antiquotations are in use:
+  The following antiquotations are defined:
 
   \begin{itemize}
-  \item[$\bullet$] {\bf @{text "@{ML \"\<dots>\"}"}} Should be used for value
-  computations. It checks whether the ML-expression is valid ML-code, but only
-  works for closed expression.
+  \item[$\bullet$] @{text "@{ML \"\<dots>\" for \<dots> in \<dots>}"} 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:
+  
+  \begin{center}
+  \begin{tabular}{l}
+  @{text "@{ML \"1 + 3\"}"}\\
+  @{text "@{ML \"a + b\" for a b}"}\\
+  @{text "@{ML Ident in OuterLex}"}
+  \end{tabular}
+  \end{center}
 
-  \item[$\bullet$] {\bf @{text "@{ML_open \"\<dots>\" for \<dots>}"}} 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 \"\<dots>\" \"\<dots>\"}"}} The first
-  expression is checked like in the antiquotation @{text "@{ML \"\<dots>\"}"}; the
+  \item[$\bullet$] @{text "@{ML_response \"\<dots>\" \"\<dots>\"}"} should be used to
+  display ML-ex\-pressions and their response.
+  The first expression is checked like in the antiquotation @{text "@{ML \"\<dots>\"}"}; the
   second is a pattern that specifies the result the first expression
-  produces. This specification can contain @{text [quotes] "\<dots>"} for parts that
-  can be omitted. The actual response will be checked against the
-  specification. For example @{text "@{ML_response \"(1+2,3)\"
+  produces. This specification can contain @{text "\<dots>"} 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,\<dots>)\"}"}. This antiquotation can only be used when the result can be
-  constructed. It does not work when the code produces an exception or is an
-  abstract datatype (like @{ML_type thm} or @{ML_type cterm}).
+  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$] {\bf @{text "@{ML_response_fake \"\<dots>\" \"\<dots>\"}"}} Works like
+  \item[$\bullet$] @{text "@{ML_response_fake \"\<dots>\" \"\<dots>\"}"} Works like
   the @{ML_text ML_response}-anti\-quotation, except that the
-  result-specification is not checked.
+  result-specification is not checked. Use this antiquotation 
+  if the result cannot be constructed or the code generates an exception.
 
-  \item[$\bullet$] {\bf @{text "@{ML_file \"\<dots>\"}"}} Should be used when
+  \item[$\bullet$] @{text "@{ML_file \"\<dots>\"}"} 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.
+  environments. In this way they are also checked by the compiler. Some \LaTeX-hack, however, 
+  ensures that the environment markers are not printed.
 
-  \item Line numbers for code can be shown using 
-  \isacommand{ML} \isa{\%linenumbers} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}.
+  \item Line numbers can be printed using 
+  \isacommand{ML} \isa{\%linenumbers} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} 
+  for ML-code or \isacommand{lemma} \isa{\%linenumbers} @{text "..."} for proofs.
 
   \end{itemize}
 

--- a/CookBook/Recipes/Antiquotes.thy	Fri Nov 28 05:56:28 2008 +0100
+++ b/CookBook/Recipes/Antiquotes.thy	Sat Nov 29 21:20:18 2008 +0000
@@ -48,7 +48,7 @@
   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_open "(space_explode \"\\n\" txt)" for txt} 
+  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]"}).
@@ -146,7 +146,7 @@
 
   In both cases, the check by the compiler ensures that code and result match. A limitation
   of this antiquotation is that the hints can only be given for results that can actually
-  be constructed as a pattern. This excludes values that are abstract types, like 
+  be constructed as a pattern. This excludes values that are abstract datatypes, like 
   theorems or cterms.
 
 *}

--- a/CookBook/antiquote_setup.ML	Fri Nov 28 05:56:28 2008 +0100
+++ b/CookBook/antiquote_setup.ML	Sat Nov 29 21:20:18 2008 +0000
@@ -22,12 +22,12 @@
 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end";
 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option";
 
-fun output_ml_open ml src ctxt ((txt,ovars),pos) =
+fun output_ml ml src ctxt ((txt,ovars),pos) =
   (ML_Context.eval_in (SOME ctxt) false pos (ml ovars txt);
   ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt))
 
-fun output_ml ml src ctxt (txt,pos) =
-  output_ml_open (K ml) src ctxt ((txt,()),pos) 
+fun output_ml_aux ml src ctxt (txt,pos) =
+  output_ml (K ml) src ctxt ((txt,()),pos) 
 
 fun add_response_indicator txt =
   map (fn s => "> " ^ s) (space_explode "\n" txt)
@@ -48,19 +48,19 @@
   else error ("Source file " ^ quote txt ^ " does not exist.")
 
 val _ = ThyOutput.add_commands
-  [("ML_open", ThyOutput.args (Scan.lift (OuterParse.position (Args.name --
+  [("ML", ThyOutput.args (Scan.lift (OuterParse.position (Args.name --
       (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
-       Scan.optional (Args.parens (OuterParse.list1 Args.name)) [])))) (output_ml_open ml_val_open)),
+       Scan.optional (Args.$$$ "in"  |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])))) 
+                                                                 (output_ml ml_val_open)),
    ("ML_file", ThyOutput.args (Scan.lift Args.name)
       (ThyOutput.output (fn _ => fn s => (check_file_exists s; Pretty.str s)))),
    ("ML_text", ThyOutput.args (Scan.lift Args.name)
       (ThyOutput.output (fn _ => fn s => Pretty.str s))),
-   ("ML", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml ml_val)),
    ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
       (output_ml_response ml_pat)),
    ("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
       (output_ml_response_fake ml_val)),
-   ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml ml_struct)),
-   ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml ml_type))];
+   ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_struct)),
+   ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type))];
    
 end;

Binary file cookbook.pdf has changed