40   The function @{ML "(op $$)"} takes a string as argument and will ``consume'' this string from 

    40   The function @{ML "(op $$)"} takes a string as argument and will ``consume'' this string from 

    41   a given input list of strings. ``Consume'' in this context means that it will 

    41   a given input list of strings. ``Consume'' in this context means that it will 

    42   return a pair consisting of this string and the rest of the input list. 

    42   return a pair consisting of this string and the rest of the input list. 

    43   For example:

    43   For example:

    44 

    44 

    47 

    48 

    48   This function will either succeed (as in the two examples above) or raise the exception 

    49   This function will either succeed (as in the two examples above) or raise the exception 

    49   @{text "FAIL"} if no string can be consumed. For example trying to parse

    50   @{text "FAIL"} if no string can be consumed. For example trying to parse

    50 

    51 

    52                                "Exception FAIL raised"}

    53                                "Exception FAIL raised"}

    53   

    54   

    54   will raise the exception @{text "FAIL"}.

    55   will raise the exception @{text "FAIL"}.

    55   There are three exceptions used in the parsing combinators:

    56   There are three exceptions used in the parsing combinators:

    56 

    57 

    71   one item from the input list satisfying this predicate. For example the

    72   one item from the input list satisfying this predicate. For example the

    72   following parser either consumes an @{text [quotes] "h"} or a @{text

    73   following parser either consumes an @{text [quotes] "h"} or a @{text

    73   [quotes] "w"}:

    74   [quotes] "w"}:

    74 

    75 

    75 

    76 

    77 "let 

    78 "let 

    78   val hw = Scan.one (fn x => x = \"h\" orelse x = \"w\")

    79   val hw = Scan.one (fn x => x = \"h\" orelse x = \"w\")

    79   val input1 = (explode \"hello\")

    80   val input1 = (explode \"hello\")

    80   val input2 = (explode \"world\")

    81   val input2 = (explode \"world\")

    81 in

    82 in

    85 

    86 

    86   Two parser can be connected in sequence by using the function @{ML "(op --)"}. 

    87   Two parser can be connected in sequence by using the function @{ML "(op --)"}. 

    87   For example parsing @{text "h"}, @{text "e"} and @{text "l"} in this 

    88   For example parsing @{text "h"}, @{text "e"} and @{text "l"} in this 

    88   sequence can be achieved by

    89   sequence can be achieved by

    89 

    90 

    91                           "(((\"h\", \"e\"), \"l\"), [\"l\", \"o\"])"}

    92                           "(((\"h\", \"e\"), \"l\"), [\"l\", \"o\"])"}

    92 

    93 

    93   Note how the result of consumed strings builds up on the left as nested pairs.  

    94   Note how the result of consumed strings builds up on the left as nested pairs.  

    94 

    95 

    95   If, as in the previous example, one wants to parse a particular string, 

    96   If, as in the previous example, one wants to parse a particular string, 

    96   then one should use the function @{ML Scan.this_string}:

    97   then one should use the function @{ML Scan.this_string}:

    97 

    98 

    99                           "(\"hell\", [\"o\"])"}

   100                           "(\"hell\", [\"o\"])"}

   100 

   101 

   101   Parsers that explore alternatives can be constructed using the function @{ML

   102   Parsers that explore alternatives can be constructed using the function @{ML

   102   "(op ||)"}. For example, the parser @{ML "(p || q)" for p q} returns the

   103   "(op ||)"}. For example, the parser @{ML "(p || q)" for p q} returns the

   103   result of @{text "p"}, in case it succeeds, otherwise it returns the

   104   result of @{text "p"}, in case it succeeds, otherwise it returns the

   104   result of @{text "q"}. For example

   105   result of @{text "q"}. For example

   105 

   106 

   106 

   107 

   108 "let 

   109 "let 

   109   val hw = ($$ \"h\") || ($$ \"w\")

   110   val hw = ($$ \"h\") || ($$ \"w\")

   110   val input1 = (explode \"hello\")

   111   val input1 = (explode \"hello\")

   111   val input2 = (explode \"world\")

   112   val input2 = (explode \"world\")

   112 in

   113 in

   116 

   117 

   117   The functions @{ML "(op |--)"} and @{ML "(op --|)"} work like the sequencing function 

   118   The functions @{ML "(op |--)"} and @{ML "(op --|)"} work like the sequencing function 

   118   for parsers, except that they discard the item being parsed by the first (respectively second)

   119   for parsers, except that they discard the item being parsed by the first (respectively second)

   119   parser. For example

   120   parser. For example

   120   

   121   

   122 "let 

   123 "let 

   123   val just_e = ($$ \"h\") |-- ($$ \"e\") 

   124   val just_e = ($$ \"h\") |-- ($$ \"e\") 

   124   val just_h = ($$ \"h\") --| ($$ \"e\") 

   125   val just_h = ($$ \"h\") --| ($$ \"e\") 

   125   val input = (explode \"hello\")  

   126   val input = (explode \"hello\")  

   126 in 

   127 in 

   130 

   131 

   131   The parser @{ML "Scan.optional p x" for p x} returns the result of the parser 

   132   The parser @{ML "Scan.optional p x" for p x} returns the result of the parser 

   132   @{text "p"}, if it succeeds; otherwise it returns 

   133   @{text "p"}, if it succeeds; otherwise it returns 

   133   the default value @{text "x"}. For example

   134   the default value @{text "x"}. For example

   134 

   135 

   136 "let 

   137 "let 

   137   val p = Scan.optional ($$ \"h\") \"x\"

   138   val p = Scan.optional ($$ \"h\") \"x\"

   138   val input1 = (explode \"hello\")

   139   val input1 = (explode \"hello\")

   139   val input2 = (explode \"world\")  

   140   val input2 = (explode \"world\")  

   140 in 

   141 in 

   143  "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"x\", [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}

   144  "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"x\", [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}

   144 

   145 

   145   The function @{ML Scan.option} works similarly, except no default value can

   146   The function @{ML Scan.option} works similarly, except no default value can

   146   be given. Instead, the result is wrapped as an @{text "option"}-type. For example:

   147   be given. Instead, the result is wrapped as an @{text "option"}-type. For example:

   147 

   148 

   149 "let 

   150 "let 

   150   val p = Scan.option ($$ \"h\")

   151   val p = Scan.option ($$ \"h\")

   151   val input1 = (explode \"hello\")

   152   val input1 = (explode \"hello\")

   152   val input2 = (explode \"world\")  

   153   val input2 = (explode \"world\")  

   153 in 

   154 in 

   157   The function @{ML "(op !!)"} helps to produce appropriate error messages

   158   The function @{ML "(op !!)"} helps to produce appropriate error messages

   158   during parsing. For example if one wants to parse that @{text p} is immediately 

   159   during parsing. For example if one wants to parse that @{text p} is immediately 

   159   followed by @{text q}, or start a completely different parser @{text r},

   160   followed by @{text q}, or start a completely different parser @{text r},

   160   one might write

   161   one might write

   161 

   162 

   163 

   164 

   164   However, this parser is problematic for producing an appropriate error message, in case

   165   However, this parser is problematic for producing an appropriate error message, in case

   165   the parsing of @{ML "(p -- q)" for p q} fails. Because in that case one loses the information 

   166   the parsing of @{ML "(p -- q)" for p q} fails. Because in that case one loses the information 

   166   that @{text p} should be followed by @{text q}. To see this consider the case in

   167   that @{text p} should be followed by @{text q}. To see this consider the case in

   167   which @{text p} 

   168   which @{text p} 

   172   caused by the

   173   caused by the

   173   failure of @{text r}, not by the absence of @{text q} in the input. This kind of situation

   174   failure of @{text r}, not by the absence of @{text q} in the input. This kind of situation

   174   can be avoided when using the function @{ML "(op !!)"}. This function aborts the whole process of

   175   can be avoided when using the function @{ML "(op !!)"}. This function aborts the whole process of

   175   parsing in case of a failure and prints an error message. For example if we invoke the parser

   176   parsing in case of a failure and prints an error message. For example if we invoke the parser

   176   

   177   

   178 

   179 

   179   on @{text [quotes] "hello"}, the parsing succeeds

   180   on @{text [quotes] "hello"}, the parsing succeeds

   180 

   181 

   182                 "(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"hello\")" 

   183                 "(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"hello\")" 

   183                 "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}

   184                 "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}

   184 

   185 

   185   but if we invoke it on @{text [quotes] "world"}

   186   but if we invoke it on @{text [quotes] "world"}

   186   

   187   

   188                                "Exception ABORT raised"}

   189                                "Exception ABORT raised"}

   189 

   190 

   190   then the parsing aborts and the error message @{text "foo"} is printed out. In order to

   191   then the parsing aborts and the error message @{text "foo"} is printed out. In order to

   191   see the error message properly, we need to prefix the parser with the function 

   192   see the error message properly, we need to prefix the parser with the function 

   192   @{ML "Scan.error"}. For example

   193   @{ML "Scan.error"}. For example

   193 

   194 

   195                                "Exception Error \"foo\" raised"}

   196                                "Exception Error \"foo\" raised"}

   196 

   197 

   197   This ``prefixing'' is usually done by wrappers such as @{ML "OuterSyntax.command"} 

   198   This ``prefixing'' is usually done by wrappers such as @{ML "OuterSyntax.command"} 

   198   (FIXME: give reference to later place). 

   199   (FIXME: give reference to later place). 

   199   

   200   

   212 

   213 

   213 text {*

   214 text {*

   214   Running this parser with the @{text [quotes] "h"} and @{text [quotes] "e"}, and 

   215   Running this parser with the @{text [quotes] "h"} and @{text [quotes] "e"}, and 

   215   the input @{text [quotes] "holle"} 

   216   the input @{text [quotes] "holle"} 

   216 

   217 

   218                                "Exception ERROR \"h is not followed by e\" raised"} 

   219                                "Exception ERROR \"h is not followed by e\" raised"} 

   219 

   220 

   220   produces the correct error message. Running it with

   221   produces the correct error message. Running it with

   221  

   222  

   223                           "((\"w\", \"w\"), [\"o\", \"r\", \"l\", \"d\"])"}

   224                           "((\"w\", \"w\"), [\"o\", \"r\", \"l\", \"d\"])"}

   224   

   225   

   225   yields the expected parsing. 

   226   yields the expected parsing. 

   226 

   227 

   227   The function @{ML "Scan.repeat p" for p} will apply a parser @{text p} as 

   228   The function @{ML "Scan.repeat p" for p} will apply a parser @{text p} as 

   228   often as it succeeds. For example

   229   often as it succeeds. For example

   229   

   230   

   231                 "([\"h\", \"h\", \"h\", \"h\"], [\"e\", \"l\", \"l\", \"o\"])"}

   232                 "([\"h\", \"h\", \"h\", \"h\"], [\"e\", \"l\", \"l\", \"o\"])"}

   232   

   233   

   233   Note that @{ML "Scan.repeat"} stores the parsed items in a list. The function

   234   Note that @{ML "Scan.repeat"} stores the parsed items in a list. The function

   234   @{ML "Scan.repeat1"} is similar, but requires that the parser @{text "p"} 

   235   @{ML "Scan.repeat1"} is similar, but requires that the parser @{text "p"} 

   235   succeeds at least once.

   236   succeeds at least once.

   237   Also note that the parser would have aborted with the exception @{text MORE}, if

   238   Also note that the parser would have aborted with the exception @{text MORE}, if

   238   we had run it only on just @{text [quotes] "hhhh"}. This can be avoided by using

   239   we had run it only on just @{text [quotes] "hhhh"}. This can be avoided by using

   239   the wrapper @{ML Scan.finite} and the ``stopper-token'' @{ML Symbol.stopper}. With

   240   the wrapper @{ML Scan.finite} and the ``stopper-token'' @{ML Symbol.stopper}. With

   240   them we can write

   241   them we can write

   241   

   242   

   243                 "([\"h\", \"h\", \"h\", \"h\"], [])"}

   244                 "([\"h\", \"h\", \"h\", \"h\"], [])"}

   244 

   245 

   245   @{ML Symbol.stopper} is the ``end-of-input'' indicator for parsing strings;

   246   @{ML Symbol.stopper} is the ``end-of-input'' indicator for parsing strings;

   246   other stoppers need to be used when parsing token, for example. However, this kind of 

   247   other stoppers need to be used when parsing token, for example. However, this kind of 

   247   manually wrapping is often already done by the surrounding infrastructure. 

   248   manually wrapping is often already done by the surrounding infrastructure. 

   248 

   249 

   249   The function @{ML Scan.repeat} can be used with @{ML Scan.one} to read any 

   250   The function @{ML Scan.repeat} can be used with @{ML Scan.one} to read any 

   250   string as in

   251   string as in

   251 

   252 

   253 "let 

   254 "let 

   254    val p = Scan.repeat (Scan.one Symbol.not_eof)

   255    val p = Scan.repeat (Scan.one Symbol.not_eof)

   255    val input = (explode \"foo bar foo\") 

   256    val input = (explode \"foo bar foo\") 

   256 in

   257 in

   257    Scan.finite Symbol.stopper p input

   258    Scan.finite Symbol.stopper p input

   262   end of the input string (i.e.~stopper symbol).

   263   end of the input string (i.e.~stopper symbol).

   263 

   264 

   264   The function @{ML "Scan.unless p q" for p q} takes two parsers: if the first one can 

   265   The function @{ML "Scan.unless p q" for p q} takes two parsers: if the first one can 

   265   parse the input, then the whole parser fails; if not, then the second is tried. Therefore

   266   parse the input, then the whole parser fails; if not, then the second is tried. Therefore

   266   

   267   

   268                                "Exception FAIL raised"}

   269                                "Exception FAIL raised"}

   269 

   270 

   270   fails, while

   271   fails, while

   271 

   272 

   273                           "(\"w\",[\"o\", \"r\", \"l\", \"d\"])"}

   274                           "(\"w\",[\"o\", \"r\", \"l\", \"d\"])"}

   274 

   275 

   275   succeeds. 

   276   succeeds. 

   276 

   277 

   277   The functions @{ML Scan.repeat} and @{ML Scan.unless} can be combined to read any

   278   The functions @{ML Scan.repeat} and @{ML Scan.unless} can be combined to read any

   278   input until a certain marker symbol is reached. In the example below the marker

   279   input until a certain marker symbol is reached. In the example below the marker

   279   symbol is a @{text [quotes] "*"}.

   280   symbol is a @{text [quotes] "*"}.

   280 

   281 

   282 "let 

   283 "let 

   283   val p = Scan.repeat (Scan.unless ($$ \"*\") (Scan.one Symbol.not_eof))

   284   val p = Scan.repeat (Scan.unless ($$ \"*\") (Scan.one Symbol.not_eof))

   284   val input1 = (explode \"fooooo\")

   285   val input1 = (explode \"fooooo\")

   285   val input2 = (explode \"foo*ooo\")

   286   val input2 = (explode \"foo*ooo\")

   286 in

   287 in

   293   After parsing is done, one nearly always wants to apply a function on the parsed 

   294   After parsing is done, one nearly always wants to apply a function on the parsed 

   294   items. To do this the function @{ML "(p >> f)" for p f} can be employed, which runs 

   295   items. To do this the function @{ML "(p >> f)" for p f} can be employed, which runs 

   295   first the parser @{text p} and upon successful completion applies the 

   296   first the parser @{text p} and upon successful completion applies the 

   296   function @{text f} to the result. For example

   297   function @{text f} to the result. For example

   297 

   298 

   299 "let 

   300 "let 

   300   fun double (x,y) = (x^x,y^y) 

   301   fun double (x,y) = (x^x,y^y) 

   301 in

   302 in

   302   (($$ \"h\") -- ($$ \"e\") >> double) (explode \"hello\")

   303   (($$ \"h\") -- ($$ \"e\") >> double) (explode \"hello\")

   303 end"

   304 end"

   304 "((\"hh\", \"ee\"), [\"l\", \"l\", \"o\"])"}

   305 "((\"hh\", \"ee\"), [\"l\", \"l\", \"o\"])"}

   305 

   306 

   306   doubles the two parsed input strings. Or

   307   doubles the two parsed input strings. Or

   307 

   308 

   309 "let 

   310 "let 

   310    val p = Scan.repeat (Scan.one Symbol.not_eof) >> implode

   311    val p = Scan.repeat (Scan.one Symbol.not_eof) >> implode

   311    val input = (explode \"foo bar foo\") 

   312    val input = (explode \"foo bar foo\") 

   312 in

   313 in

   313    Scan.finite Symbol.stopper p input

   314    Scan.finite Symbol.stopper p input

   328 

   329 

   329   The function @{ML Scan.lift} takes a parser and a pair as arguments. This function applies

   330   The function @{ML Scan.lift} takes a parser and a pair as arguments. This function applies

   330   the given parser to the second component of the pair and leaves the  first component 

   331   the given parser to the second component of the pair and leaves the  first component 

   331   untouched. For example

   332   untouched. For example

   332 

   333 

   334 "Scan.lift (($$ \"h\") -- ($$ \"e\")) (1,(explode \"hello\"))"

   335 "Scan.lift (($$ \"h\") -- ($$ \"e\")) (1,(explode \"hello\"))"

   335 "((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}

   336 "((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}

   336 

   337 

   337   (FIXME: In which situations is this useful? Give examples.) 

   338   (FIXME: In which situations is this useful? Give examples.) 

   338 *}

   339 *}

   363   the function @{ML "OuterSyntax.scan"}, which we give below @{ML

   364   the function @{ML "OuterSyntax.scan"}, which we give below @{ML

   364   "Position.none"} as argument since, at the moment, we are not interested in

   365   "Position.none"} as argument since, at the moment, we are not interested in

   365   generating precise error messages. The following

   366   generating precise error messages. The following

   366 

   367 

   367 

   368 

   369 "[Token (\<dots>,(Ident, \"hello\"),\<dots>), 

   370 "[Token (\<dots>,(Ident, \"hello\"),\<dots>), 

   370  Token (\<dots>,(Space, \" \"),\<dots>), 

   371  Token (\<dots>,(Space, \" \"),\<dots>), 

   371  Token (\<dots>,(Ident, \"world\"),\<dots>)]"}

   372  Token (\<dots>,(Ident, \"world\"),\<dots>)]"}

   372 

   373 

   373   produces three tokens where the first and the last are identifiers, since

   374   produces three tokens where the first and the last are identifiers, since

   379   Many parsing functions later on will require spaces, comments and the like

   380   Many parsing functions later on will require spaces, comments and the like

   380   to have already been filtered out.  So from now on we are going to use the 

   381   to have already been filtered out.  So from now on we are going to use the 

   381   functions @{ML filter} and @{ML OuterLex.is_proper} do this. For example

   382   functions @{ML filter} and @{ML OuterLex.is_proper} do this. For example

   382 

   383 

   383 

   384 

   385 "let

   386 "let

   386    val input = OuterSyntax.scan Position.none \"hello world\"

   387    val input = OuterSyntax.scan Position.none \"hello world\"

   387 in

   388 in

   388    filter OuterLex.is_proper input

   389    filter OuterLex.is_proper input

   389 end" 

   390 end" 

   398 

   399 

   399 text {*

   400 text {*

   400 

   401 

   401   If we parse

   402   If we parse

   402 

   403 

   404 "filtered_input \"inductive | for\"" 

   405 "filtered_input \"inductive | for\"" 

   405 "[Token (\<dots>,(Command, \"inductive\"),\<dots>), 

   406 "[Token (\<dots>,(Command, \"inductive\"),\<dots>), 

   406  Token (\<dots>,(Keyword, \"|\"),\<dots>), 

   407  Token (\<dots>,(Keyword, \"|\"),\<dots>), 

   407  Token (\<dots>,(Keyword, \"for\"),\<dots>)]"}

   408  Token (\<dots>,(Keyword, \"for\"),\<dots>)]"}

   408 

   409 

   409   we obtain a list consisting of only a command and two keyword tokens.

   410   we obtain a list consisting of only a command and two keyword tokens.

   410   If you want to see which keywords and commands are currently known, type in

   411   If you want to see which keywords and commands are currently known, type in

   411   the following (you might have to adjust the @{ML print_depth} in order to

   412   the following (you might have to adjust the @{ML print_depth} in order to

   412   see the complete list):

   413   see the complete list):

   413 

   414 

   415 "let 

   416 "let 

   416   val (keywords, commands) = OuterKeyword.get_lexicons ()

   417   val (keywords, commands) = OuterKeyword.get_lexicons ()

   417 in 

   418 in 

   418   (Scan.dest_lexicon commands, Scan.dest_lexicon keywords)

   419   (Scan.dest_lexicon commands, Scan.dest_lexicon keywords)

   419 end" 

   420 end" 

   420 "([\"}\",\"{\",\<dots>],[\"\<rightleftharpoons>\",\"\<leftharpoondown>\",\<dots>])"}

   421 "([\"}\",\"{\",\<dots>],[\"\<rightleftharpoons>\",\"\<leftharpoondown>\",\<dots>])"}

   421 

   422 

   422   Now the parser @{ML "OuterParse.$$$"} parses a single keyword. For example

   423   Now the parser @{ML "OuterParse.$$$"} parses a single keyword. For example

   423 

   424 

   425 "let 

   426 "let 

   426   val input1 = filtered_input \"where for\"

   427   val input1 = filtered_input \"where for\"

   427   val input2 = filtered_input \"| in\"

   428   val input2 = filtered_input \"| in\"

   428 in 

   429 in 

   429   (OuterParse.$$$ \"where\" input1, OuterParse.$$$ \"|\" input2)

   430   (OuterParse.$$$ \"where\" input1, OuterParse.$$$ \"|\" input2)

   430 end"

   431 end"

   431 "((\"where\",\<dots>),(\"|\",\<dots>))"}

   432 "((\"where\",\<dots>),(\"|\",\<dots>))"}

   432 

   433 

   433   Like before, we can sequentially connect parsers with @{ML "(op --)"}. For example 

   434   Like before, we can sequentially connect parsers with @{ML "(op --)"}. For example 

   434 

   435 

   436 "let 

   437 "let 

   437   val input = filtered_input \"| in\"

   438   val input = filtered_input \"| in\"

   438 in 

   439 in 

   439   (OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\") input

   440   (OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\") input

   440 end"

   441 end"

   442 

   443 

   443   The parser @{ML "OuterParse.enum s p" for s p} parses a possibly empty 

   444   The parser @{ML "OuterParse.enum s p" for s p} parses a possibly empty 

   444   list of items recognised by the parser @{text p}, where the items being parsed

   445   list of items recognised by the parser @{text p}, where the items being parsed

   445   are separated by the string @{text s}. For example

   446   are separated by the string @{text s}. For example

   446 

   447 

   448 "let 

   449 "let 

   449   val input = filtered_input \"in | in | in foo\"

   450   val input = filtered_input \"in | in | in foo\"

   450 in 

   451 in 

   451   (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input

   452   (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input

   452 end" 

   453 end" 

   458   and then failed with the exception @{text "MORE"}. Like in the previous

   459   and then failed with the exception @{text "MORE"}. Like in the previous

   459   section, we can avoid this exception using the wrapper @{ML

   460   section, we can avoid this exception using the wrapper @{ML

   460   Scan.finite}. This time, however, we have to use the ``stopper-token'' @{ML

   461   Scan.finite}. This time, however, we have to use the ``stopper-token'' @{ML

   461   OuterLex.stopper}. We can write

   462   OuterLex.stopper}. We can write

   462 

   463 

   464 "let 

   465 "let 

   465   val input = filtered_input \"in | in | in\"

   466   val input = filtered_input \"in | in | in\"

   466 in 

   467 in 

   467   Scan.finite OuterLex.stopper 

   468   Scan.finite OuterLex.stopper 

   468          (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input

   469          (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input

   480   The function @{ML "OuterParse.!!!"} can be used to force termination of the

   481   The function @{ML "OuterParse.!!!"} can be used to force termination of the

   481   parser in case of a dead end, just like @{ML "Scan.!!"} (see previous section), 

   482   parser in case of a dead end, just like @{ML "Scan.!!"} (see previous section), 

   482   except that the error message is fixed to be @{text [quotes] "Outer syntax error"}

   483   except that the error message is fixed to be @{text [quotes] "Outer syntax error"}

   483   with a relatively precise description of the failure. For example:

   484   with a relatively precise description of the failure. For example:

   484 

   485 

   486 "let 

   487 "let 

   487   val input = filtered_input \"in |\"

   488   val input = filtered_input \"in |\"

   488   val parse_bar_then_in = OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\"

   489   val parse_bar_then_in = OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\"

   489 in 

   490 in 

   490   parse (OuterParse.!!! parse_bar_then_in) input 

   491   parse (OuterParse.!!! parse_bar_then_in) input 

   726 end *}

   727 end *}

   727 

   728 

   728 text {*

   729 text {*

   729   Now we can type for example

   730   Now we can type for example

   730 

   731 

   732   

   733   

   733   and see the proposition in the tracing buffer.  

   734   and see the proposition in the tracing buffer.  

   734 

   735 

   735   Note that so far we used @{ML thy_decl in OuterKeyword} as kind indicator

   736   Note that so far we used @{ML thy_decl in OuterKeyword} as kind indicator

   736   for the command.  This means that the command finishes as soon as the

   737   for the command.  This means that the command finishes as soon as the

   772   11 contain the parser for the proposition.

   773   11 contain the parser for the proposition.

   773 

   774 

   774   If we now type @{text "foobar \"True \<and> True\""}, we obtain the following 

   775   If we now type @{text "foobar \"True \<and> True\""}, we obtain the following 

   775   proof state:

   776   proof state:

   776  

   777  

   778 "goal (1 subgoal):

   779 "goal (1 subgoal):

   779 1. True \<and> True"}

   780 1. True \<and> True"}

   780 

   781 

   781   and we can build the proof

   782   and we can build the proof

   782 

   783 

   784 apply(rule conjI)

   785 apply(rule conjI)

   785 apply(rule TrueI)+

   786 apply(rule TrueI)+

   786 done"} 

   787 done"} 

   787   

   788   

   788   (FIXME What does @{text "Toplevel.theory"}?)

   789   (FIXME What does @{text "Toplevel.theory"}?)