ProgTutorial/Solutions.thy
changeset 458 242e81f4d461
parent 447 d21cea8e0bcf
child 469 7a558c5119b2
equal deleted inserted replaced
457:aedfdcae39a9 458:242e81f4d461
    81   @{ML scan_all} retruns a string, instead of the pair a parser would
    81   @{ML scan_all} retruns a string, instead of the pair a parser would
    82   normally return. For example:
    82   normally return. For example:
    83 
    83 
    84   @{ML_response [display,gray]
    84   @{ML_response [display,gray]
    85 "let
    85 "let
    86   val input1 = (explode \"foo bar\")
    86   val input1 = (Symbol.explode \"foo bar\")
    87   val input2 = (explode \"foo (*test*) bar (*test*)\")
    87   val input2 = (Symbol.explode \"foo (*test*) bar (*test*)\")
    88 in
    88 in
    89   (scan_all input1, scan_all input2)
    89   (scan_all input1, scan_all input2)
    90 end"
    90 end"
    91 "(\"foo bar\", \"foo (**test**) bar (**test**)\")"}
    91 "(\"foo bar\", \"foo (**test**) bar (**test**)\")"}
    92 *}
    92 *}