CookBook/Parsing.thy
changeset 132 2d9198bcb850
parent 131 8db9195bb3e9
child 133 3e94ccc0f31e
equal deleted inserted replaced
131:8db9195bb3e9 132:2d9198bcb850
   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