CookBook/Solutions.thy
changeset 80 95e9c4556221
parent 72 7b8c4fe235aa
child 130 a21d7b300616
equal deleted inserted replaced
79:a53c7810e38b 80:95e9c4556221
    39 text {*
    39 text {*
    40   By using @{text "#> fst"} in the last line, the function 
    40   By using @{text "#> fst"} in the last line, the function 
    41   @{ML scan_all} retruns a string, instead of the pair a parser would
    41   @{ML scan_all} retruns a string, instead of the pair a parser would
    42   normally return. For example:
    42   normally return. For example:
    43 
    43 
    44   @{ML_response [display,gray] "scan_all (explode \"foo bar\")" "\"foo bar\""}
    44   @{ML_response [display,gray]
    45 
    45 "let
    46   @{ML_response [display,gray] "scan_all (explode \"foo (*test*) bar (*test*)\")" 
    46    val input1 = (explode \"foo bar\")
    47                           "\"foo (**test**) bar (**test**)\""}
    47    val input2 = (explode \"foo (*test*) bar (*test*)\")
    48 
    48  in
       
    49    (scan_all input1, scan_all input2)
       
    50  end"
       
    51 "(\"foo bar\",\"foo (**test**) bar (**test**)\")"}
    49 *}
    52 *}
    50 
    53 
    51 end
    54 end