CookBook/Parsing.thy
changeset 54 1783211b3494
parent 53 0c3580c831a4
child 56 126646f2aa88
equal deleted inserted replaced
53:0c3580c831a4 54:1783211b3494
   397   Scan.finite OuterLex.stopper 
   397   Scan.finite OuterLex.stopper 
   398          (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input
   398          (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input
   399 end" 
   399 end" 
   400 "([\"in\",\"in\",\"in\"],[])"}
   400 "([\"in\",\"in\",\"in\"],[])"}
   401 
   401 
   402   The following function will help us to run examples
   402   The following function will help us later to run examples
   403 
   403 
   404 *}
   404 *}
   405 
   405 
   406 ML {*
   406 ML {*
   407 fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input
   407 fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input
   425 but keyword in was found\" raised"
   425 but keyword in was found\" raised"
   426 }
   426 }
   427 
   427 
   428   \begin{exercise}
   428   \begin{exercise}
   429   A type-identifier, for example @{typ "'a"}, is a token of 
   429   A type-identifier, for example @{typ "'a"}, is a token of 
   430   kind @{ML "Keyword" in OuterLex} can be parsed 
   430   kind @{ML "Keyword" in OuterLex}. It can be parsed using 
   431 
   431   the function @{ML OuterParse.type_ident}.
   432   \end{exercise}
   432   \end{exercise}
   433 
   433 
   434 
   434 
   435 *}
   435 *}
   436 
   436