isabelle-cookbook: comparison CookBook/Parsing.thy

equal deleted inserted replaced

-:2d9198bcb850
+:3e94ccc0f31e
 r}. If you want to generate the correct error message for p-followed-by-q,
 then you have to write:
 *}
 ML{*fun p_followed_by_q p q r =
 let
 val err_msg = (fn _ => p ^ " is not followed by " ^ q)
 in
 ($$ p -- (!! err_msg ($$ q))) || ($$ r -- $$ r)
 end *}
 text {*
 Running this parser with the @{text [quotes] "h"} and @{text [quotes] "e"}, and
 the input @{text [quotes] "holle"}
 section {* Parsing Theory Syntax *}
 text {*
 Most of the time, however, Isabelle developers have to deal with parsing
-tokens, not strings.  These token parsers will have the type
+tokens, not strings.  These token parsers will have the type:
 *}
 ML{*type 'a parser = OuterLex.token list -> 'a * OuterLex.token list*}
 text {*
 end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"}
 The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of
 @{ML thm_name in SpecParse}. Theorem names can contain attributes. The name
 has to end with @{text [quotes] ":"}---see the argument of
-@{ML SpecParse.opt_thm_name} in Line 9.
+the function @{ML SpecParse.opt_thm_name} in Line 9.
 \begin{readmore}
 Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"}
 and @{ML_file "Pure/Isar/args.ML"}.
 \end{readmore}