isabelle-cookbook: comparison ProgTutorial/Parsing.thy

equal deleted inserted replaced

-:6e2479089226
+:cecd7a941885
 imports Base "Package/Simple_Inductive_Package"
 keywords "foobar" "foobar_trace" :: thy_decl and
 "foobar_goal" "foobar_prove" :: thy_goal
 begin
-chapter {* Parsing\label{chp:parsing} *}
+chapter \<open>Parsing\label{chp:parsing}\<close>
-text {*
+text \<open>
 \begin{flushright}
 {\em An important principle underlying the success and popularity of Unix\\ is
 the philosophy of building on the work of others.} \\[1ex]
 Tony Travis in an email about the\\ ``LINUX is obsolete'' debate
 \end{flushright}
 "Pure/Isar/parse.ML"}. In addition specific parsers for packages are
 defined in @{ML_file "Pure/Isar/parse_spec.ML"}. Parsers for method arguments
 are defined in @{ML_file "Pure/Isar/args.ML"}.
 \end{readmore}
-*}
+\<close>
-section {* Building Generic Parsers *}
+section \<open>Building Generic Parsers\<close>
-text {*
+text \<open>
 Let us first have a look at parsing strings using generic parsing
 combinators. The function @{ML_ind "$$" in Scan} takes a string as argument and will
 ``consume'' this string from a given input list of strings. ``Consume'' in
 this context means that it will return a pair consisting of this string and
 @{ML_response [display,gray]
 "($$ \"w\") (Symbol.explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"}
 The function @{ML "$$"} will either succeed (as in the two examples above)
-or raise the exception @{text "FAIL"} if no string can be consumed. For
+or raise the exception \<open>FAIL\<close> if no string can be consumed. For
 example trying to parse
 @{ML_response_fake [display,gray]
 "($$ \"x\") (Symbol.explode \"world\")"
 "Exception FAIL raised"}
-will raise the exception @{text "FAIL"}. The function @{ML_ind "$$" in Scan} will also
+will raise the exception \<open>FAIL\<close>. The function @{ML_ind "$$" in Scan} will also
 fail if you try to consume more than a single character.
 There are three exceptions that are raised by the parsing combinators:
 \begin{itemize}
-\item @{text "FAIL"} indicates that alternative routes of parsing
+\item \<open>FAIL\<close> indicates that alternative routes of parsing
 might be explored.
-\item @{text "MORE"} indicates that there is not enough input for the parser. For example
+\item \<open>MORE\<close> indicates that there is not enough input for the parser. For example
-in @{text "($$ \"h\") []"}.
+in \<open>($$ "h") []\<close>.
-\item @{text "ABORT"} indicates that a dead end is reached.
+\item \<open>ABORT\<close> indicates that a dead end is reached.
 It is used for example in the function @{ML "!!"} (see below).
 \end{itemize}
 However, note that these exceptions are private to the parser and cannot be accessed
 by the programmer (for example to handle them).
 In the examples above we use the function @{ML_ind explode in Symbol} from the
 structure @{ML_struct Symbol}, instead of the more standard library function
 @{ML_ind explode in String}, for obtaining an input list for the parser. The reason is
 that @{ML explode in Symbol} is aware of character
-sequences, for example @{text "\<foo>"}, that have a special meaning in
+sequences, for example \<open>\<foo>\<close>, that have a special meaning in
 Isabelle. To see the difference consider
 @{ML_response_fake [display,gray]
 "let
 val input = \"\<foo> bar\"
 (hw input1, hw input2)
 end"
 "((\"h\", [\"e\", \"l\", \"l\", \"o\"]),(\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
 Two parsers can be connected in sequence by using the function @{ML_ind "--" in Scan}.
-For example parsing @{text "h"}, @{text "e"} and @{text "l"} (in this
+For example parsing \<open>h\<close>, \<open>e\<close> and \<open>l\<close> (in this
 order) you can achieve by:
 @{ML_response [display,gray]
 "($$ \"h\" -- $$ \"e\" -- $$ \"l\") (Symbol.explode \"hello\")"
 "(((\"h\", \"e\"), \"l\"), [\"l\", \"o\"])"}
 "Scan.this_string \"hell\" (Symbol.explode \"hello\")"
 "(\"hell\", [\"o\"])"}
 Parsers that explore alternatives can be constructed using the function
 @{ML_ind  "||" in Scan}. The parser @{ML "(p || q)" for p q} returns the
-result of @{text "p"}, in case it succeeds; otherwise it returns the
+result of \<open>p\<close>, in case it succeeds; otherwise it returns the
-result of @{text "q"}. For example:
+result of \<open>q\<close>. For example:
 @{ML_response [display,gray]
 "let
 val hw = $$ \"h\" || $$ \"w\"
 (just_e input, just_h input)
 end"
 "((\"e\", [\"l\", \"l\", \"o\"]), (\"h\", [\"l\", \"l\", \"o\"]))"}
 The parser @{ML "Scan.optional p x" for p x} returns the result of the parser
-@{text "p"}, in case it succeeds; otherwise it returns
+\<open>p\<close>, in case it succeeds; otherwise it returns
-the default value @{text "x"}. For example:
+the default value \<open>x\<close>. For example:
 @{ML_response [display,gray]
 "let
 val p = Scan.optional ($$ \"h\") \"x\"
 val input1 = Symbol.explode \"hello\"
 (p input1, p input2)
 end"
 "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"x\", [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
 The function @{ML_ind option in Scan} works similarly, except no default value can
-be given. Instead, the result is wrapped as an @{text "option"}-type. For example:
+be given. Instead, the result is wrapped as an \<open>option\<close>-type. For example:
 @{ML_response [display,gray]
 "let
 val p = Scan.option ($$ \"h\")
 val input1 = Symbol.explode \"hello\"
 @{ML_response [display,gray]
 "Scan.ahead (Scan.this_string \"foo\") (Symbol.explode \"foo\")"
 "(\"foo\", [\"f\", \"o\", \"o\"])"}
 The function @{ML_ind "!!" in Scan} helps with producing appropriate error messages
-during parsing. For example if you want to parse @{text p} immediately
+during parsing. For example if you want to parse \<open>p\<close> immediately
-followed by @{text q}, or start a completely different parser @{text r},
+followed by \<open>q\<close>, or start a completely different parser \<open>r\<close>,
 you might write:
 @{ML [display,gray] "(p -- q) || r" for p q r}
 However, this parser is problematic for producing a useful error
 message, if the parsing of @{ML "(p -- q)" for p q} fails. Because with the
-parser above you lose the information that @{text p} should be followed by @{text q}.
+parser above you lose the information that \<open>p\<close> should be followed by \<open>q\<close>.
-To see this assume that @{text p} is present in the input, but it is not
+To see this assume that \<open>p\<close> is present in the input, but it is not
-followed by @{text q}. That means @{ML "(p -- q)" for p q} will fail and
+followed by \<open>q\<close>. That means @{ML "(p -- q)" for p q} will fail and
-hence the alternative parser @{text r} will be tried. However, in many
+hence the alternative parser \<open>r\<close> will be tried. However, in many
-circumstances this will be the wrong parser for the input ``@{text "p"}-followed-by-something''
+circumstances this will be the wrong parser for the input ``\<open>p\<close>-followed-by-something''
 and therefore will also fail. The error message is then caused by the failure
-of @{text r}, not by the absence of @{text q} in the input. Such
+of \<open>r\<close>, not by the absence of \<open>q\<close> in the input. Such
 situation can be avoided when using the function @{ML "!!"}.  This function
 aborts the whole process of parsing in case of a failure and prints an error
 message. For example if you invoke the parser
 but if you invoke it on @{text [quotes] "world"}
 @{ML_response_fake [display,gray] "(!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"
 "Exception ABORT raised"}
-then the parsing aborts and the error message @{text "foo"} is printed. In order to
+then the parsing aborts and the error message \<open>foo\<close> is printed. In order to
 see the error message properly, you need to prefix the parser with the function
 @{ML_ind error in Scan}. For example:
 @{ML_response_fake [display,gray]
 "Scan.error (!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"
 such as @{ML_ind local_theory in Outer_Syntax}
 (see Section~\ref{sec:newcommand} which explains this function in more detail).
 Let us now return to our example of parsing @{ML "(p -- q) || r" for p q
 r}. If you want to generate the correct error message for failure
-of parsing @{text "p"}-followed-by-@{text "q"}, then you have to write:
+of parsing \<open>p\<close>-followed-by-\<open>q\<close>, then you have to write:
-*}
+\<close>
-ML %grayML{*fun p_followed_by_q p q r =
+ML %grayML\<open>fun p_followed_by_q p q r =
 let
 val err_msg = fn _ => p ^ " is not followed by " ^ q
 in
 ($$ p -- (!! (fn _ => err_msg) ($$ q))) || ($$ r -- $$ r)
-end *}
+end\<close>
-text {*
+text \<open>
 Running this parser with the arguments
 @{text [quotes] "h"}, @{text [quotes] "e"} and @{text [quotes] "w"}, and
 the input @{text [quotes] "holle"}
 @{ML_response_fake [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (Symbol.explode \"holle\")"
 @{ML_response [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (Symbol.explode \"wworld\")"
 "((\"w\", \"w\"), [\"o\", \"r\", \"l\", \"d\"])"}
 yields the expected parsing.
-The function @{ML "Scan.repeat p" for p} will apply a parser @{text p} as
+The function @{ML "Scan.repeat p" for p} will apply a parser \<open>p\<close> as
 long as it succeeds. For example:
 @{ML_response [display,gray] "Scan.repeat ($$ \"h\") (Symbol.explode \"hhhhello\")"
 "([\"h\", \"h\", \"h\", \"h\"], [\"e\", \"l\", \"l\", \"o\"])"}
 Note that @{ML_ind repeat in Scan} stores the parsed items in a list. The function
-@{ML_ind repeat1 in Scan} is similar, but requires that the parser @{text "p"}
+@{ML_ind repeat1 in Scan} is similar, but requires that the parser \<open>p\<close>
 succeeds at least once.
-Also note that the parser would have aborted with the exception @{text MORE}, if
+Also note that the parser would have aborted with the exception \<open>MORE\<close>, if
 you had it run with the string @{text [quotes] "hhhh"}. This can be avoided by using
 the wrapper @{ML_ind finite in Scan} and the ``stopper-token''
 @{ML_ind stopper in Symbol}. With them you can write:
 @{ML_response [display,gray] "Scan.finite Symbol.stopper (Scan.repeat ($$ \"h\")) (Symbol.explode \"hhhh\")"
 After parsing is done, you almost always want to apply a function to the parsed
 items. One way to do this is the function @{ML_ind ">>" in Scan} where
 @{ML "(p >> f)" for p f} runs
-first the parser @{text p} and upon successful completion applies the
+first the parser \<open>p\<close> and upon successful completion applies the
-function @{text f} to the result. For example
+function \<open>f\<close> to the result. For example
 @{ML_response [display,gray]
 "let
 fun double (x, y) = (x ^ x, y ^ y)
 val parser = $$ \"h\" -- $$ \"e\"
 @{ML_response [display,gray]
 "Scan.lift ($$ \"h\" -- $$ \"e\") (1, Symbol.explode \"hello\")"
 "((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}
-\footnote{\bf FIXME: In which situations is @{text "lift"} useful? Give examples.}
+\footnote{\bf FIXME: In which situations is \<open>lift\<close> useful? Give examples.}
 Be aware of recursive parsers. Suppose you want to read strings separated by
 commas and by parentheses into a tree datastructure; for example, generating
 the tree corresponding to the string @{text [quotes] "(A, A), (A, A)"} where
-the @{text "A"}s will be the leaves.  We assume the trees are represented by the
+the \<open>A\<close>s will be the leaves.  We assume the trees are represented by the
 datatype:
-*}
+\<close>
-ML %grayML{*datatype tree =
+ML %grayML\<open>datatype tree =
 Lf of string
-| Br of tree * tree*}
+| Br of tree * tree\<close>
-text {*
+text \<open>
 Since nested parentheses should be treated in a meaningful way---for example
 the string @{text [quotes] "((A))"} should be read into a single
 leaf---you might implement the following parser.
-*}
+\<close>
-ML %grayML{*fun parse_basic s =
+ML %grayML\<open>fun parse_basic s =
 $$ s >> Lf || $$ "(" |-- parse_tree s --| $$ ")"
 and parse_tree s =
-parse_basic s --| $$ "," -- parse_tree s >> Br || parse_basic s*}
+parse_basic s --| $$ "," -- parse_tree s >> Br || parse_basic s\<close>
-text {*
+text \<open>
 This parser corresponds to the grammar:
 \begin{center}
 \begin{tabular}{lcl}
-@{text "<Basic>"}  & @{text "::="} & @{text "<String> | (<Tree>)"}\\
+\<open><Basic>\<close>  & \<open>::=\<close> & \<open><String> | (<Tree>)\<close>\\
-@{text "<Tree>"}   & @{text "::="} & @{text "<Basic>, <Tree> | <Basic>"}\\
+\<open><Tree>\<close>   & \<open>::=\<close> & \<open><Basic>, <Tree> | <Basic>\<close>\\
 \end{tabular}
 \end{center}
-The parameter @{text "s"} is the string over which the tree is parsed. The
+The parameter \<open>s\<close> is the string over which the tree is parsed. The
 parser @{ML parse_basic} reads either a leaf or a tree enclosed in
 parentheses. The parser @{ML parse_tree} reads either a pair of trees
 separated by a comma, or acts like @{ML parse_basic}. Unfortunately,
 because of the mutual recursion, this parser will immediately run into a
 loop, even if it is called without any input. For example
 looping parser are not useful, because of ML's strict evaluation of
 arguments. Therefore we need to delay the execution of the
 parser until an input is given. This can be done by adding the parsed
 string as an explicit argument. So the parser above should be implemented
 as follows.
-*}
+\<close>
-ML %grayML{*fun parse_basic s xs =
+ML %grayML\<open>fun parse_basic s xs =
 ($$ s >> Lf || $$ "(" |-- parse_tree s --| $$ ")") xs
 and parse_tree s xs =
-(parse_basic s --| $$ "," -- parse_tree s >> Br || parse_basic s) xs*}
+(parse_basic s --| $$ "," -- parse_tree s >> Br || parse_basic s) xs\<close>
-text {*
+text \<open>
 While the type of the parser is unchanged by the addition, its behaviour
 changed: with this version of the parser the execution is delayed until
-some string is  applied for the argument @{text "xs"}. This gives us
+some string is  applied for the argument \<open>xs\<close>. This gives us
 exactly the parser what we wanted. An example is as follows:
 @{ML_response [display, gray]
 "let
 val input = Symbol.explode \"(A,((A))),A\"
 "(Br (Br (Lf \"A\", Lf \"A\"), Lf \"A\"), [])"}
 \begin{exercise}\label{ex:scancmts}
 Write a parser that parses an input string so that any comment enclosed
-within @{text "(*\<dots>*)"} is replaced by the same comment but enclosed within
+within \<open>(*\<dots>*)\<close> is replaced by the same comment but enclosed within
-@{text "(**\<dots>**)"} in the output string. To enclose a string, you can use the
+\<open>(**\<dots>**)\<close> 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}. Hint: To simplify the task ignore the proper
 nesting of comments.
 \end{exercise}
-*}
+\<close>
-section {* Parsing Theory Syntax *}
+section \<open>Parsing Theory Syntax\<close>
-text {*
+text \<open>
 Most of the time, however, Isabelle developers have to deal with parsing
 tokens, not strings.  These token parsers have the type:
-*}
+\<close>
-ML %grayML{*type 'a parser = Token.T list -> 'a * Token.T list*}
+ML %grayML\<open>type 'a parser = Token.T list -> 'a * Token.T list\<close>
 ML "Thy_Header.get_keywords'"
-text {*
+text \<open>
 {\bf REDO!!}
 The reason for using token parsers is that theory syntax, as well as the
 parsers for the arguments of proof methods, use the type @{ML_type
 @{text [quotes] "hello"} and @{text [quotes] "world"} do not match any
 other syntactic category. The second indicates a space.
 We can easily change what is recognised as a keyword with the function
 @{ML_ind add_keywords in Thy_Header}. For example calling it with
-*}
+\<close>
-setup {* Thy_Header.add_keywords [(("hello", Position.none),Keyword.no_spec)] *}
+setup \<open>Thy_Header.add_keywords [(("hello", Position.none),Keyword.no_spec)]\<close>
-text {*
+text \<open>
 then lexing @{text [quotes] "hello world"} will produce
 @{ML_response_fake [display,gray] "Token.explode
 (Thy_Header.get_keywords' @{context}) Position.none \"hello world\""
 "[Token (\<dots>,(Keyword, \"hello\"),\<dots>),
 filter Token.is_proper input
 end"
 "[Token (\<dots>,(Ident, \"hello\"), \<dots>), Token (\<dots>,(Ident, \"world\"), \<dots>)]"}
 For convenience we define the function:
-*}
+\<close>
-ML %grayML{*fun filtered_input str =
+ML %grayML\<open>fun filtered_input str =
-filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) Position.none str) *}
+filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) Position.none str)\<close>
 ML \<open>filtered_input "inductive | for"\<close>
-text {*
+text \<open>
 If you now parse
 @{ML_response_fake [display,gray]
 "filtered_input \"inductive | for\""
 "[Token (\<dots>,(Command, \"inductive\"),\<dots>),
 you obtain a list consisting of only one command and two keyword tokens.
 If you want to see which keywords and commands are currently known to Isabelle,
 use the function @{ML_ind get_keywords' in Thy_Header}:
-You might have to adjust the @{text ML_print_depth} in order to
+You might have to adjust the \<open>ML_print_depth\<close> in order to
 see the complete list.
 The parser @{ML_ind "$$$" in Parse} parses a single keyword. For example:
 @{ML_response [display,gray]
 (Parse.$$$ \"|\" -- Parse.$$$ \"in\") input
 end"
 "((\"|\", \"in\"), [])"}
 The parser @{ML "Parse.enum s p" for s p} parses a possibly empty
-list of items recognised by the parser @{text p}, where the items being parsed
+list of items recognised by the parser \<open>p\<close>, where the items being parsed
-are separated by the string @{text s}. For example:
+are separated by the string \<open>s\<close>. For example:
 @{ML_response [display,gray]
 "let
 val input = filtered_input \"in | in | in foo\"
 in
 "([\"in\", \"in\", \"in\"], [\<dots>])"}
 The function @{ML_ind enum1 in Parse} works similarly, except that the
 parsed list must be non-empty. Note that we had to add a string @{text
 [quotes] "foo"} at the end of the parsed string, otherwise the parser would
-have consumed all tokens and then failed with the exception @{text
+have consumed all tokens and then failed with the exception \<open>MORE\<close>. Like in the previous section, we can avoid this exception using the
-"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 Token.stopper}. We can write:
 @{ML_response [display,gray]
 "let
 Scan.finite Token.stopper p input
 end"
 "([\"in\", \"in\", \"in\"], [])"}
 The following function will help to run examples.
-*}
+\<close>
-ML %grayML{*fun parse p input = Scan.finite Token.stopper (Scan.error p) input *}
+ML %grayML\<open>fun parse p input = Scan.finite Token.stopper (Scan.error p) input\<close>
-text {*
+text \<open>
 The function @{ML_ind "!!!" in Parse} can be used to force termination
 of the parser in case of a dead end, just like @{ML "Scan.!!"} (see previous
 section). A difference, however, is that the error message of @{ML
 "Parse.!!!"} is fixed to be @{text [quotes] "Outer syntax error"}
 together with a relatively precise description of the failure. For example:
 Whenever there is a possibility that the processing of user input can fail,
 it is a good idea to give all available information about where the error
 occurred. For this Isabelle can attach positional information to tokens
 and then thread this information up the ``processing chain''. To see this,
 modify the function @{ML filtered_input}, described earlier, as follows
-*}
+\<close>
-ML %grayML{*fun filtered_input' str =
+ML %grayML\<open>fun filtered_input' str =
-filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) (Position.line 7) str) *}
+filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) (Position.line 7) str)\<close>
-text {*
+text \<open>
 where we pretend the parsed string starts on line 7. An example is
 @{ML_response_fake [display,gray]
 "filtered_input' \"foo \\n bar\""
 "[Token ((\"foo\", ({line=7, end_line=7}, {line=7})), (Ident, \"foo\"), \<dots>),
 binds stronger than addition, and both of them nest to the right.
 The context-free grammar is defined as:
 \begin{center}
 \begin{tabular}{lcl}
-@{text "<Basic>"}  & @{text "::="} & @{text "<Number> | (<Expr>)"}\\
+\<open><Basic>\<close>  & \<open>::=\<close> & \<open><Number> | (<Expr>)\<close>\\
-@{text "<Factor>"} & @{text "::="} & @{text "<Basic> * <Factor> | <Basic>"}\\
+\<open><Factor>\<close> & \<open>::=\<close> & \<open><Basic> * <Factor> | <Basic>\<close>\\
-@{text "<Expr>"}   & @{text "::="} & @{text "<Factor> + <Expr>  | <Factor>"}\\
+\<open><Expr>\<close>   & \<open>::=\<close> & \<open><Factor> + <Expr>  | <Factor>\<close>\\
 \end{tabular}
 \end{center}
 Hint: Be careful with recursive parsers.
 \end{exercise}
-*}
+\<close>
-section {* Parsers for ML-Code (TBD) *}
+section \<open>Parsers for ML-Code (TBD)\<close>
-text {*
+text \<open>
 @{ML_ind ML_source in Parse}
-*}
+\<close>
-section {* Context Parser (TBD) *}
+section \<open>Context Parser (TBD)\<close>
-text {*
+text \<open>
 @{ML_ind Args.context}
-*}
+\<close>
 (*
 ML {*
 let
 val parser = Args.context -- Scan.lift Args.name_inner_syntax
 |> fst
 end
 *}
 *)
-text {*
+text \<open>
 @{ML_ind Args.context}
 Used for example in \isacommand{attribute\_setup} and \isacommand{method\_setup}.
-*}
+\<close>
-section {* Argument and Attribute Parsers (TBD) *}
+section \<open>Argument and Attribute Parsers (TBD)\<close>
-section {* Parsing Inner Syntax *}
+section \<open>Parsing Inner Syntax\<close>
-text {*
+text \<open>
 There is usually no need to write your own parser for parsing inner syntax, that is
 for terms and  types: you can just call the predefined parsers. Terms can
 be parsed using the function @{ML_ind term in Parse}. For example:
 @{ML_response_fake [display,gray]
 @{ML_ind parse_term in Syntax} @{ML_ind check_term in Syntax}
 @{ML_ind parse_typ in Syntax} @{ML_ind check_typ in Syntax}
 @{ML_ind read_term in Syntax} @{ML_ind read_term in Syntax}
-*}
+\<close>
-section {* Parsing Specifications\label{sec:parsingspecs} *}
+section \<open>Parsing Specifications\label{sec:parsingspecs}\<close>
-text {*
+text \<open>
 There are a number of special purpose parsers that help with parsing
 specifications of function definitions, inductive predicates and so on. In
 Chapter~\ref{chp:package}, for example, we will need to parse specifications
 for inductive predicates of the form:
-*}
+\<close>
 simple_inductive
 even and odd
 where
 even0: "even 0"
 | evenS: "odd n \<Longrightarrow> even (Suc n)"
 | oddS: "even n \<Longrightarrow> odd (Suc n)"
-text {*
+text \<open>
 For this we are going to use the parser:
-*}
+\<close>
-ML %linenosgray{*val spec_parser =
+ML %linenosgray\<open>val spec_parser =
 Parse.vars --
 Scan.optional
 (Parse.$$$ "where" |--
 Parse.!!!
 (Parse.enum1 "|"
-(Parse_Spec.opt_thm_name ":" -- Parse.prop))) []*}
+(Parse_Spec.opt_thm_name ":" -- Parse.prop))) []\<close>
-text {*
+text \<open>
 Note that the parser must not parse the keyword \simpleinductive, even if it is
 meant to process definitions as shown above. The parser of the keyword
 will be given by the infrastructure that will eventually call @{ML spec_parser}.
 end"
 "(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
 [((even0,\<dots>),\<dots>),
 ((evenS,\<dots>),\<dots>),
 ((oddS,\<dots>),\<dots>)]), [])"}
-*}
+\<close>
 ML \<open>let
 val input = filtered_input
 "foo::\"int \<Rightarrow> bool\" and bar::nat (\"BAR\" 100) and blonk"
 in
 parse Parse.vars input
 end\<close>
-text {*
+text \<open>
 As you see, the result is a pair consisting of a list of
 variables with optional type-annotation and syntax-annotation, and a list of
 rules where every rule has optionally a name and an attribute.
 The function @{ML_ind "vars" in Parse} in Line 2 of the parser reads an
 \isacommand{and}-separated
 list of variables that can include optional type annotations and syntax translations.
 For example:\footnote{Note that in the code we need to write
-@{text "\\\"int \<Rightarrow> bool\\\""} in order to properly escape the double quotes
+\<open>\"int \<Rightarrow> bool\"\<close> in order to properly escape the double quotes
 in the compound type.}
 @{ML_response_fake [display,gray]
 "let
 val input = filtered_input
 parse Parse.vars input
 end"
 "([(foo, SOME \<dots>, NoSyn),
 (bar, SOME \<dots>, Mixfix (Source {text=\"BAR\",...}, [], 100, \<dots>)),
 (blonk, NONE, NoSyn)],[])"}
-*}
+\<close>
-text {*
+text \<open>
 Whenever types are given, they are stored in the @{ML SOME}s. The types are
 not yet used to type the variables: this must be done by type-inference later
 on. Since types are part of the inner syntax they are strings with some
 encoded information (see previous section). If a mixfix-syntax is
 present for a variable, then it is stored in the
 \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}
-*}
+\<close>
-text_raw {*
+text_raw \<open>
 \begin{exercise}
 Have a look at how the parser @{ML Parse_Spec.where_multi_specs} is implemented
 in file @{ML_file "Pure/Isar/parse_spec.ML"}. This parser corresponds
 to the ``where-part'' of the introduction rules given above. Below
 we paraphrase the code of @{ML_ind where_multi_specs in Parse_Spec} adapted to our
 purposes.
 \begin{isabelle}
-*}
+\<close>
-ML %linenosgray{*val spec_parser' =
+ML %linenosgray\<open>val spec_parser' =
 Parse.vars --
 Scan.optional
 (Parse.$$$ "where" |--
 Parse.!!!
 (Parse.enum1 "|"
 ((Parse_Spec.opt_thm_name ":" -- Parse.prop) --|
 Scan.option (Scan.ahead (Parse.name ||
 Parse.$$$ "[") --
-Parse.!!! (Parse.$$$ "|"))))) [] *}
+Parse.!!! (Parse.$$$ "|"))))) []\<close>
-text_raw {*
+text_raw \<open>
 \end{isabelle}
 Both parsers accept the same input% that's not true:
 % spec_parser accepts input that is refuted by spec_parser'
 , but if you look closely, you can notice
 an additional  ``tail'' (Lines 8 to 10) in @{ML spec_parser'}. What is the purpose of
 this additional ``tail''?
 \end{exercise}
-*}
+\<close>
-text {*
+text \<open>
 (FIXME: @{ML Parse.type_args}, @{ML Parse.typ}, @{ML Parse.opt_mixfix})
-*}
+\<close>
-section {* New Commands\label{sec:newcommand} *}
+section \<open>New Commands\label{sec:newcommand}\<close>
-text {*
+text \<open>
 Often new commands, for example for providing new definitional principles,
 need to be implemented. While this is not difficult on the ML-level and for
 jEdit, in order to be backwards compatible, new commands need also to be recognised
 by Proof-General. This results in some subtle configuration issues, which we will
 explain in the next section. Here we just describe how to define new commands
 implement any new command, you have to ``announce'' it in the
 \isacommand{keywords}-section of your theory header. For \isacommand{foobar}
 we need to write something like
 \begin{graybox}
-\isacommand{theory}~@{text Foo}\\
+\isacommand{theory}~\<open>Foo\<close>\\
-\isacommand{imports}~@{text Main}\\
+\isacommand{imports}~\<open>Main\<close>\\
-\isacommand{keywords} @{text [quotes] "foobar"} @{text "::"} @{text "thy_decl"}\\
+\isacommand{keywords} @{text [quotes] "foobar"} \<open>::\<close> \<open>thy_decl\<close>\\
 ...
 \end{graybox}
 where @{ML_ind "thy_decl" in Keyword} indicates the kind of the
-command.  Another possible kind is @{text "thy_goal"}, or you can
+command.  Another possible kind is \<open>thy_goal\<close>, or you can
 also omit the kind entirely, in which case you declare a keyword
 (something that is part of a command).
 Now you can implement \isacommand{foobar} as follows.
-*}
+\<close>
-ML %grayML{*let
+ML %grayML\<open>let
 val do_nothing = Scan.succeed (Local_Theory.background_theory I)
 in
 Outer_Syntax.local_theory @{command_keyword "foobar"}
 "description of foobar"
 do_nothing
-end *}
+end\<close>
-text {*
+text \<open>
 The crucial function @{ML_ind local_theory in Outer_Syntax} expects
 the name for the command, a kind indicator, a short description and
 a parser producing a local theory transition (explained later). For the
-name and the kind, you can use the ML-antiquotation @{text "@{command_spec ...}"}.
+name and the kind, you can use the ML-antiquotation \<open>@{command_spec ...}\<close>.
 You can now write in your theory
-*}
+\<close>
 foobar
-text {*
+text \<open>
 but of course you will not see anything since \isacommand{foobar} is
 not intended to do anything.  Remember, however, that this only
 works in jEdit. In order to enable also Proof-General recognise this
 command, a keyword file needs to be generated (see next section).
 us refine it a bit next by letting it take a proposition as argument
 and printing this proposition inside the tracing buffer. We announce
 the command \isacommand{foobar\_trace} in the theory header as
 \begin{graybox}
-\isacommand{keywords} @{text [quotes] "foobar_trace"} @{text "::"} @{text "thy_decl"}
+\isacommand{keywords} @{text [quotes] "foobar_trace"} \<open>::\<close> \<open>thy_decl\<close>
 \end{graybox}
 The crucial part of a command is the function that determines the
 behaviour of the command. In the code above we used a
 ``do-nothing''-function, which because of the parser @{ML_ind succeed in Scan}
 does not parse any argument, but immediately returns the simple
 function @{ML "Local_Theory.background_theory I"}. We can replace
 this code by a function that first parses a proposition (using the
 parser @{ML Parse.prop}), then prints out some tracing information
-(using the function @{text trace_prop}) and finally does
+(using the function \<open>trace_prop\<close>) and finally does
 nothing. For this you can write:
-*}
+\<close>
-ML %grayML{*let
+ML %grayML\<open>let
 fun trace_prop str =
 Local_Theory.background_theory (fn ctxt => (tracing str; ctxt))
 in
 Outer_Syntax.local_theory @{command_keyword "foobar_trace"}
 "traces a proposition"
 (Parse.prop >> trace_prop)
-end *}
+end\<close>
-text {*
+text \<open>
 This command can now be used to
 see the proposition in the tracing buffer.
-*}
+\<close>
 foobar_trace "True \<and> False"
-text {*
+text \<open>
 Note that so far we used @{ML_ind thy_decl in Keyword} as the kind
 indicator for the new command.  This means that the command finishes as soon as
 the arguments are processed. Examples of this kind of commands are
 \isacommand{definition} and \isacommand{declare}.  In other cases, commands
 are expected to parse some arguments, for example a proposition, and then
 the kind indicator @{ML_ind thy_goal in Keyword} and the function @{ML
 "local_theory_to_proof" in Outer_Syntax} to set up the command.
 Below we show the command \isacommand{foobar\_goal} which takes a
 proposition as argument and then starts a proof in order to prove
 it. Therefore, we need to announce this command in the header
-as @{text "thy_goal"}.
+as \<open>thy_goal\<close>.
 \begin{graybox}
-\isacommand{keywords} @{text [quotes] "foobar_goal"} @{text "::"} @{text "thy_goal"}
+\isacommand{keywords} @{text [quotes] "foobar_goal"} \<open>::\<close> \<open>thy_goal\<close>
 \end{graybox}
 Then we can write:
-*}
+\<close>
-ML%linenosgray{*let
+ML%linenosgray\<open>let
 fun goal_prop str ctxt =
 let
 val prop = Syntax.read_prop ctxt str
 in
 Proof.theorem NONE (K I) [[(prop, [])]] ctxt
 end
 in
 Outer_Syntax.local_theory_to_proof @{command_keyword "foobar_goal"}
 "proves a proposition"
 (Parse.prop >> goal_prop)
-end *}
+end\<close>
-text {*
+text \<open>
-The function @{text goal_prop} in Lines 2 to 7 takes a string (the proposition to be
+The function \<open>goal_prop\<close> in Lines 2 to 7 takes a string (the proposition to be
 proved) and a context as argument.  The context is necessary in order to be able to use
 @{ML_ind read_prop in Syntax}, which converts a string into a proper proposition.
 In Line 6 the function @{ML_ind theorem in Proof} starts the proof for the
 proposition. Its argument @{ML NONE} stands for a locale (which we chose to
 omit); the argument @{ML "(K I)"} stands for a function that determines what
 should be done with the theorem once it is proved (we chose to just forget
 about it).
 If you now type \isacommand{foobar\_goal}~@{text [quotes] "True \<and> True"},
 you obtain the following proof state:
-*}
+\<close>
 foobar_goal "True \<and> True"
-txt {*
+txt \<open>
 \begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}\medskip
 and can prove the proposition as follows.
-*}
+\<close>
 apply(rule conjI)
 apply(rule TrueI)+
 done
-text {*
+text \<open>
 The last command we describe here is
 \isacommand{foobar\_proof}. Like \isacommand{foobar\_goal}, its purpose is
 to take a proposition and open a corresponding proof-state that
 allows us to give a proof for it. However, unlike
 \isacommand{foobar\_goal}, the proposition will be given as a
 text as ML-source and then interpret it as an Isabelle term using
 the ML-runtime.  For the parsing part, we can use the function
 @{ML_ind "ML_source" in Parse} in the structure @{ML_struct
 Parse}. For running the ML-interpreter we need the following
 scaffolding code.
-*}
+\<close>
-ML %grayML{*
+ML %grayML\<open>
 structure Result = Proof_Data
 (type T = unit -> term
 fun init thy () = error "Result")
-val result_cookie = (Result.get, Result.put, "Result.put") *}
+val result_cookie = (Result.get, Result.put, "Result.put")\<close>
-text {*
+text \<open>
 With this in place, we can implement the code for \isacommand{foobar\_prove}
 as follows.
-*}
+\<close>
-ML %linenosgray{*let
+ML %linenosgray\<open>let
 fun after_qed thm_name thms lthy =
 Local_Theory.note (thm_name, (flat thms)) lthy |> snd
 fun setup_proof (thm_name, src) lthy =
 let
 val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source
 in
 Outer_Syntax.local_theory_to_proof @{command_keyword "foobar_prove"}
 "proving a proposition"
 (parser >> setup_proof)
-end*}
+end\<close>
-text {*
+text \<open>
 In Line 12, we implement a parser that first reads in an optional lemma name (terminated
 by ``:'') and then some ML-code. The function in Lines 5 to 10 takes the ML-text
 and lets the ML-runtime evaluate it using the function @{ML_ind value in Code_Runtime}
 in the structure @{ML_struct Code_Runtime}.  Once the ML-text has been turned into a term,
 the function @{ML theorem in Proof} opens a corresponding proof-state. This function takes the
-function @{text "after_qed"} as argument, whose purpose is to store the theorem
+function \<open>after_qed\<close> as argument, whose purpose is to store the theorem
-(once it is proven) under the given name @{text "thm_name"}.
+(once it is proven) under the given name \<open>thm_name\<close>.
 You can now define a term, for example
-*}
+\<close>
-ML %grayML{*val prop_true = @{prop "True"}*}
+ML %grayML\<open>val prop_true = @{prop "True"}\<close>
-text {*
+text \<open>
 and give it a proof using \isacommand{foobar\_prove}:
-*}
+\<close>
 foobar_prove test: prop_true
 apply(rule TrueI)
 done
-text {*
+text \<open>
 Finally you can test whether the lemma has been stored under the given name.
 \begin{isabelle}
-\isacommand{thm}~@{text "test"}\\
+\isacommand{thm}~\<open>test\<close>\\
-@{text "> "}~@{thm TrueI}
+\<open>> \<close>~@{thm TrueI}
 \end{isabelle}
-*}
+\<close>
 (*
 text {*
 {\bf TBD below}
 ML {*
 Context.set_thread_data (SOME (let fun tactic (facts: thm list) : tactic =  (atac 1)   in Context.map_proof (Method.set_tactic tactic) end (ML_Context.the_generic_context ())));
 *}
 *)
-section {* Methods (TBD) *}
+section \<open>Methods (TBD)\<close>
-text {*
+text \<open>
 (FIXME: maybe move to after the tactic section)
 Methods are central to Isabelle. You use them, for example,
 in \isacommand{apply}. To print out all currently known methods you can use the
 Isabelle command:
 \begin{isabelle}
 \isacommand{print\_methods}\\
-@{text "> methods:"}\\
+\<open>> methods:\<close>\\
-@{text ">   -:  do nothing (insert current facts only)"}\\
+\<open>>   -:  do nothing (insert current facts only)\<close>\\
-@{text ">   HOL.default:  apply some intro/elim rule (potentially classical)"}\\
+\<open>>   HOL.default:  apply some intro/elim rule (potentially classical)\<close>\\
-@{text ">   ..."}
+\<open>>   ...\<close>
 \end{isabelle}
 An example of a very simple method is:
-*}
+\<close>
 method_setup %gray foo =
-{* Scan.succeed
+\<open>Scan.succeed
-(fn ctxt => (SIMPLE_METHOD ((eresolve_tac ctxt [@{thm conjE}] THEN' resolve_tac ctxt [@{thm conjI}]) 1))) *}
+(fn ctxt => (SIMPLE_METHOD ((eresolve_tac ctxt [@{thm conjE}] THEN' resolve_tac ctxt [@{thm conjI}]) 1)))\<close>
 "foo method for conjE and conjI"
-text {*
+text \<open>
-It defines the method @{text foo}, which takes no arguments (therefore the
+It defines the method \<open>foo\<close>, which takes no arguments (therefore the
 parser @{ML Scan.succeed}) and only applies a single tactic, namely the tactic which
 applies @{thm [source] conjE} and then @{thm [source] conjI}. The function
 @{ML_ind SIMPLE_METHOD in Method}
-turns such a tactic into a method. The method @{text "foo"} can be used as follows
+turns such a tactic into a method. The method \<open>foo\<close> can be used as follows
-*}
+\<close>
 lemma shows "A \<and> B \<Longrightarrow> C \<and> D"
 apply(foo)
-txt {*
+txt \<open>
 where it results in the goal state
 \begin{minipage}{\textwidth}
 @{subgoals}
-\end{minipage} *}
+\end{minipage}\<close>
 (*<*)oops(*>*)
-method_setup test = {*
+method_setup test = \<open>
-Scan.lift (Scan.succeed (K Method.succeed)) *} {* bla *}
+Scan.lift (Scan.succeed (K Method.succeed))\<close> \<open>bla\<close>
 lemma "True"
 apply(test)
 oops
-method_setup joker = {*
+method_setup joker = \<open>
-Scan.lift (Scan.succeed (fn ctxt => Method.cheating true)) *} {* bla *}
+Scan.lift (Scan.succeed (fn ctxt => Method.cheating true))\<close> \<open>bla\<close>
 lemma "False"
 apply(joker)
 oops
-text {* if true is set then always works *}
+text \<open>if true is set then always works\<close>
-ML {* assume_tac *}
+ML \<open>assume_tac\<close>
-method_setup first_atac = {* Scan.lift (Scan.succeed (fn ctxt => (SIMPLE_METHOD (assume_tac ctxt 1)))) *} {* bla *}
+method_setup first_atac = \<open>Scan.lift (Scan.succeed (fn ctxt => (SIMPLE_METHOD (assume_tac ctxt 1))))\<close> \<open>bla\<close>
-ML {* HEADGOAL *}
+ML \<open>HEADGOAL\<close>
 lemma "A \<Longrightarrow> A"
 apply(first_atac)
 oops
-method_setup my_atac = {* Scan.lift (Scan.succeed (fn ctxt => (SIMPLE_METHOD' (assume_tac ctxt)))) *} {* bla *}
+method_setup my_atac = \<open>Scan.lift (Scan.succeed (fn ctxt => (SIMPLE_METHOD' (assume_tac ctxt))))\<close> \<open>bla\<close>
 lemma "A \<Longrightarrow> A"
 apply(my_atac)
 oops
 ML {* METHOD *}
 ML {* K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1)) *}
 ML {* Scan.succeed  *}
 *)
-ML {* resolve_tac *}
+ML \<open>resolve_tac\<close>
 method_setup myrule =
-{* Scan.lift (Scan.succeed (fn ctxt => (METHOD (fn thms => resolve_tac ctxt thms 1)))) *}
+\<open>Scan.lift (Scan.succeed (fn ctxt => (METHOD (fn thms => resolve_tac ctxt thms 1))))\<close>
-{* bla *}
+\<open>bla\<close>
 lemma
 assumes a: "A \<Longrightarrow> B \<Longrightarrow> C"
 shows "C"
 using a
 apply(myrule)
 oops
-text {*
+text \<open>
 (********************************************************)
 (FIXME: explain a version of rule-tac)
-*}
+\<close>
 end

changeset 565	cecd7a941885
parent 563	50d3059de9c6
child 566	6103b0eadbf2