
diff -r 6103b0eadbf2 -r f7c97e64cc2a ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Tue May 14 17:45:13 2019 +0200
+++ b/ProgTutorial/Parsing.thy	Thu May 16 19:56:12 2019 +0200
@@ -38,10 +38,10 @@
   \begin{readmore}
   The library for writing parser combinators is split up, roughly, into two
   parts: The first part consists of a collection of generic parser combinators
-  defined in the structure @{ML_struct Scan} in the file @{ML_file
+  defined in the structure @{ML_structure Scan} in the file @{ML_file
   "Pure/General/scan.ML"}. The second part of the library consists of
   combinators for dealing with specific token types, which are defined in the
-  structure @{ML_struct Parse} in the file @{ML_file
+  structure @{ML_structure Parse} in the file @{ML_file
   "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"}.
@@ -59,17 +59,17 @@
   this context means that it will return a pair consisting of this string and
   the rest of the input list. For example:
 
-  @{ML_response [display,gray] 
+  @{ML_matchresult [display,gray] 
   "($$ \"h\") (Symbol.explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
 
-  @{ML_response [display,gray] 
+  @{ML_matchresult [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 \<open>FAIL\<close> if no string can be consumed. For
   example trying to parse
 
-  @{ML_response_fake [display,gray] 
+  @{ML_matchresult_fake [display,gray] 
   "($$ \"x\") (Symbol.explode \"world\")" 
   "Exception FAIL raised"}
   
@@ -91,13 +91,13 @@
   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
+  structure @{ML_structure 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 \<open>\<foo>\<close>, that have a special meaning in
   Isabelle. To see the difference consider
 
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let 
   val input = \"\<foo> bar\"
 in
@@ -113,7 +113,7 @@
   following parser either consumes an @{text [quotes] "h"} or a @{text
   [quotes] "w"}:
 
-@{ML_response [display,gray] 
+@{ML_matchresult [display,gray] 
 "let 
   val hw = Scan.one (fn x => x = \"h\" orelse x = \"w\")
   val input1 = Symbol.explode \"hello\"
@@ -127,7 +127,7 @@
   For example parsing \<open>h\<close>, \<open>e\<close> and \<open>l\<close> (in this 
   order) you can achieve by:
 
-  @{ML_response [display,gray] 
+  @{ML_matchresult [display,gray] 
   "($$ \"h\" -- $$ \"e\" -- $$ \"l\") (Symbol.explode \"hello\")"
   "(((\"h\", \"e\"), \"l\"), [\"l\", \"o\"])"}
 
@@ -136,7 +136,7 @@
   If, as in the previous example, you want to parse a particular string, 
   then you can use the function @{ML_ind this_string in Scan}.
 
-  @{ML_response [display,gray] 
+  @{ML_matchresult [display,gray] 
   "Scan.this_string \"hell\" (Symbol.explode \"hello\")"
   "(\"hell\", [\"o\"])"}
 
@@ -146,7 +146,7 @@
   result of \<open>q\<close>. For example:
 
 
-@{ML_response [display,gray] 
+@{ML_matchresult [display,gray] 
 "let 
   val hw = $$ \"h\" || $$ \"w\"
   val input1 = Symbol.explode \"hello\"
@@ -162,7 +162,7 @@
   one that @{ML_ind "|--" in Scan} and @{ML_ind "--|" in Scan} ``point'' away.
   For example:
   
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
 "let 
   val just_e = $$ \"h\" |-- $$ \"e\" 
   val just_h = $$ \"h\" --| $$ \"e\" 
@@ -176,7 +176,7 @@
   \<open>p\<close>, in case it succeeds; otherwise it returns 
   the default value \<open>x\<close>. For example:
 
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
 "let 
   val p = Scan.optional ($$ \"h\") \"x\"
   val input1 = Symbol.explode \"hello\"
@@ -189,7 +189,7 @@
   The function @{ML_ind option in Scan} works similarly, except no default value can
   be given. Instead, the result is wrapped as an \<open>option\<close>-type. For example:
 
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
 "let 
   val p = Scan.option ($$ \"h\")
   val input1 = Symbol.explode \"hello\"
@@ -201,7 +201,7 @@
   The function @{ML_ind ahead in Scan} parses some input, but leaves the original
   input unchanged. For example:
 
-  @{ML_response [display,gray]
+  @{ML_matchresult [display,gray]
   "Scan.ahead (Scan.this_string \"foo\") (Symbol.explode \"foo\")" 
   "(\"foo\", [\"f\", \"o\", \"o\"])"} 
 
@@ -230,20 +230,20 @@
 
   on @{text [quotes] "hello"}, the parsing succeeds
 
-  @{ML_response [display,gray] 
+  @{ML_matchresult [display,gray] 
   "(!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"hello\")" 
   "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
 
   but if you invoke it on @{text [quotes] "world"}
 
-  @{ML_response_fake [display,gray] "(!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"
+  @{ML_matchresult_fake [display,gray] "(!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"
                                "Exception ABORT raised"}
 
   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] 
+  @{ML_matchresult_fake [display,gray] 
   "Scan.error (!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"
   "Exception Error \"foo\" raised"}
 
@@ -269,12 +269,12 @@
   @{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_matchresult_fake [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (Symbol.explode \"holle\")"
                                "Exception ERROR \"h is not followed by e\" raised"} 
 
   produces the correct error message. Running it with
  
-  @{ML_response [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (Symbol.explode \"wworld\")"
+  @{ML_matchresult [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (Symbol.explode \"wworld\")"
                           "((\"w\", \"w\"), [\"o\", \"r\", \"l\", \"d\"])"}
   
   yields the expected parsing. 
@@ -282,7 +282,7 @@
   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\")" 
+  @{ML_matchresult [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
@@ -294,7 +294,7 @@
   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\")" 
+  @{ML_matchresult [display,gray] "Scan.finite Symbol.stopper (Scan.repeat ($$ \"h\")) (Symbol.explode \"hhhh\")" 
                 "([\"h\", \"h\", \"h\", \"h\"], [])"}
 
   The function @{ML stopper in Symbol} is the ``end-of-input'' indicator for parsing strings;
@@ -304,7 +304,7 @@
   The function @{ML_ind repeat in Scan} can be used with @{ML_ind one in Scan} to read any 
   string as in
 
-  @{ML_response [display,gray] 
+  @{ML_matchresult [display,gray] 
 "let 
    val p = Scan.repeat (Scan.one Symbol.not_eof)
    val input = Symbol.explode \"foo bar foo\"
@@ -319,12 +319,12 @@
   The function @{ML_ind unless in Scan} takes two parsers: if the first one can 
   parse the input, then the whole parser fails; if not, then the second is tried. Therefore
   
-  @{ML_response_fake_both [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"hello\")"
+  @{ML_matchresult_fake_both [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"hello\")"
                                "Exception FAIL raised"}
 
   fails, while
 
-  @{ML_response [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"world\")"
+  @{ML_matchresult [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"world\")"
                           "(\"w\",[\"o\", \"r\", \"l\", \"d\"])"}
 
   succeeds. 
@@ -333,7 +333,7 @@
   be combined to read any input until a certain marker symbol is reached. In the 
   example below the marker symbol is a @{text [quotes] "*"}.
 
-  @{ML_response [display,gray]
+  @{ML_matchresult [display,gray]
 "let 
   val p = Scan.repeat (Scan.unless ($$ \"*\") (Scan.one Symbol.not_eof))
   val input1 = Symbol.explode \"fooooo\"
@@ -352,7 +352,7 @@
   first the parser \<open>p\<close> and upon successful completion applies the 
   function \<open>f\<close> to the result. For example
 
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
 "let 
   fun double (x, y) = (x ^ x, y ^ y) 
   val parser = $$ \"h\" -- $$ \"e\"
@@ -363,7 +363,7 @@
 
   doubles the two parsed input strings; or
 
-  @{ML_response [display,gray] 
+  @{ML_matchresult [display,gray] 
 "let 
    val p = Scan.repeat (Scan.one Symbol.not_eof)
    val input = Symbol.explode \"foo bar foo\" 
@@ -379,7 +379,7 @@
   the given parser to the second component of the pair and leaves the  first component 
   untouched. For example
 
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
 "Scan.lift ($$ \"h\" -- $$ \"e\") (1, Symbol.explode \"hello\")"
 "((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}
 
@@ -425,7 +425,7 @@
   because of the mutual recursion, this parser will immediately run into a
   loop, even if it is called without any input. For example
 
-  @{ML_response_fake_both [display, gray]
+  @{ML_matchresult_fake_both [display, gray]
   "parse_tree \"A\""
   "*** Exception- TOPLEVEL_ERROR raised"}
 
@@ -449,7 +449,7 @@
   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]
+  @{ML_matchresult [display, gray]
   "let
   val input = Symbol.explode \"(A,((A))),A\"
 in
@@ -487,11 +487,11 @@
 
   \begin{readmore}
   The parser functions for the theory syntax are contained in the structure
-  @{ML_struct Parse} defined in the file @{ML_file  "Pure/Isar/parse.ML"}.
+  @{ML_structure Parse} defined in the file @{ML_file  "Pure/Isar/parse.ML"}.
   The definition for tokens is in the file @{ML_file "Pure/Isar/token.ML"}.
   \end{readmore}
 
-  The structure @{ML_struct  Token} defines several kinds of tokens (for
+  The structure @{ML_structure  Token} defines several kinds of tokens (for
   example @{ML_ind Ident in Token} for identifiers, @{ML Keyword in
   Token} for keywords and @{ML_ind Command in Token} for commands). Some
   token parsers take into account the kind of tokens. The first example shows
@@ -502,7 +502,7 @@
   messages. The following code
 
 
-@{ML_response_fake [display,gray] \<open>Token.explode 
+@{ML_matchresult_fake [display,gray] \<open>Token.explode 
   (Thy_Header.get_keywords' @{context}) Position.none "hello world"\<close>
 \<open>[Token (_,(Ident, "hello"),_), 
  Token (_,(Space, " "),_), 
@@ -524,7 +524,7 @@
 text \<open>
   then lexing @{text [quotes] "hello world"} will produce
 
-  @{ML_response_fake [display,gray] "Token.explode 
+  @{ML_matchresult_fake [display,gray] "Token.explode 
   (Thy_Header.get_keywords' @{context}) Position.none \"hello world\"" 
 "[Token (_,(Keyword, \"hello\"),_), 
  Token (_,(Space, \" \"),_), 
@@ -535,7 +535,7 @@
   functions @{ML filter} and @{ML_ind is_proper in Token} to do this. 
   For example:
 
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
    val input = Token.explode (Thy_Header.get_keywords' @{context}) Position.none \"hello world\"
 in
@@ -553,7 +553,7 @@
 text \<open>
   If you now parse
 
-@{ML_response_fake [display,gray] 
+@{ML_matchresult_fake [display,gray] 
 "filtered_input \"inductive | for\"" 
 "[Token (_,(Command, \"inductive\"),_), 
  Token (_,(Keyword, \"|\"),_), 
@@ -568,7 +568,7 @@
 
   The parser @{ML_ind "$$$" in Parse} parses a single keyword. For example:
 
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
 "let 
   val input1 = filtered_input \"where for\"
   val input2 = filtered_input \"| in\"
@@ -580,7 +580,7 @@
   Any non-keyword string can be parsed with the function @{ML_ind reserved in Parse}.
   For example:
 
-  @{ML_response [display,gray]
+  @{ML_matchresult [display,gray]
 "let 
   val p = Parse.reserved \"bar\"
   val input = filtered_input \"bar\"
@@ -591,7 +591,7 @@
 
   Like before, you can sequentially connect parsers with @{ML "--"}. For example: 
 
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
 "let 
   val input = filtered_input \"| in\"
 in 
@@ -603,7 +603,7 @@
   list of items recognised by the parser \<open>p\<close>, where the items being parsed
   are separated by the string \<open>s\<close>. For example:
 
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
 "let 
   val input = filtered_input \"in | in | in foo\"
 in 
@@ -618,7 +618,7 @@
   wrapper @{ML Scan.finite}. This time, however, we have to use the
   ``stopper-token'' @{ML Token.stopper}. We can write:
 
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
 "let 
   val input = filtered_input \"in | in | in\"
   val p = Parse.enum \"|\" (Parse.$$$ \"in\")
@@ -639,7 +639,7 @@
   "Parse.!!!"} is fixed to be @{text [quotes] "Outer syntax error"}
   together with a relatively precise description of the failure. For example:
 
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let 
   val input = filtered_input \"in |\"
   val parse_bar_then_in = Parse.$$$ \"|\" -- Parse.$$$ \"in\"
@@ -671,7 +671,7 @@
 text \<open>
   where we pretend the parsed string starts on line 7. An example is
 
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "filtered_input' \"foo \\n bar\""
 "[Token ((\"foo\", ({line=7, end_line=7}, {line=7})), (Ident, \"foo\"), _),
  Token ((\"bar\", ({line=8, end_line=8}, {line=8})), (Ident, \"bar\"), _)]"}
@@ -682,7 +682,7 @@
   By using the parser @{ML position in Parse} you can access the token 
   position and return it as part of the parser result. For example
 
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
   val input = filtered_input' \"where\"
 in 
@@ -753,7 +753,7 @@
   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_matchresult_fake [display,gray]
 "let 
   val input = Token.explode (Thy_Header.get_keywords' @{context}) Position.none \"foo\"
 in 
@@ -765,11 +765,11 @@
   The function @{ML_ind prop in Parse} is similar, except that it gives a different
   error message, when parsing fails. As you can see, the parser not just returns 
   the parsed string, but also some markup information. You can decode the
-  information with the function @{ML_ind parse in YXML} in @{ML_struct YXML}. 
+  information with the function @{ML_ind parse in YXML} in @{ML_structure YXML}. 
   The result of the decoding is an XML-tree. You can see better what is going on if
   you replace @{ML Position.none} by @{ML "Position.line 42"}, say:
 
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let 
   val input = Token.explode (Thy_Header.get_keywords' @{context}) (Position.line 42) \"foo\"
 in 
@@ -832,7 +832,7 @@
   To see what the parser returns, let us parse the string corresponding to the 
   definition of @{term even} and @{term odd}:
 
-@{ML_response [display,gray]
+@{ML_matchresult [display,gray]
 "let
   val input = filtered_input
      (\"even and odd \" ^  
@@ -868,7 +868,7 @@
   \<open>\"int \<Rightarrow> bool\"\<close> in order to properly escape the double quotes
   in the compound type.}
 
-@{ML_response_fake [display,gray]
+@{ML_matchresult_fake [display,gray]
 "let
   val input = filtered_input 
         \"foo::\\\"int \<Rightarrow> bool\\\" and bar::nat (\\\"BAR\\\" 100) and blonk\"
@@ -899,7 +899,7 @@
   parsed by @{ML_ind prop in Parse}. However, they can include an optional
   theorem name plus some attributes. For example
 
-@{ML_response [display,gray] "let 
+@{ML_matchresult [display,gray] "let 
   val input = filtered_input \"foo_lemma[intro,dest!]:\"
   val ((name, attrib), _) = parse (Parse_Spec.thm_name \":\") input 
 in 
@@ -1118,7 +1118,7 @@
   The first problem for \isacommand{foobar\_proof} is to parse some
   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
+  @{ML_ind "ML_source" in Parse} in the structure @{ML_structure
   Parse}. For running the ML-interpreter we need the following
   scaffolding code.
 \<close>
@@ -1158,7 +1158,7 @@
   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, 
+  in the structure @{ML_structure 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 \<open>after_qed\<close> as argument, whose purpose is to store the theorem
   (once it is proven) under the given name \<open>thm_name\<close>.




