equal
deleted
inserted
replaced
427 "let |
427 "let |
428 val (keywords, commands) = OuterKeyword.get_lexicons () |
428 val (keywords, commands) = OuterKeyword.get_lexicons () |
429 in |
429 in |
430 (Scan.dest_lexicon commands, Scan.dest_lexicon keywords) |
430 (Scan.dest_lexicon commands, Scan.dest_lexicon keywords) |
431 end" |
431 end" |
432 "([\"}\", \"{\", \<dots>],[\"\<rightleftharpoons>\", \"\<leftharpoondown>\", \<dots>])"} |
432 "([\"}\", \"{\", \<dots>], [\"\<rightleftharpoons>\", \"\<leftharpoondown>\", \<dots>])"} |
433 |
433 |
434 The parser @{ML "OuterParse.$$$"} parses a single keyword. For example: |
434 The parser @{ML "OuterParse.$$$"} parses a single keyword. For example: |
435 |
435 |
436 @{ML_response [display,gray] |
436 @{ML_response [display,gray] |
437 "let |
437 "let |