equal
deleted
inserted
replaced
559 in |
559 in |
560 (Scan.dest_lexicon commands, Scan.dest_lexicon keywords) |
560 (Scan.dest_lexicon commands, Scan.dest_lexicon keywords) |
561 end" |
561 end" |
562 "([\"}\", \"{\", \<dots>], [\"\<rightleftharpoons>\", \"\<leftharpoondown>\", \<dots>])"} |
562 "([\"}\", \"{\", \<dots>], [\"\<rightleftharpoons>\", \"\<leftharpoondown>\", \<dots>])"} |
563 |
563 |
564 You might have to adjust the @{ML_ind print_depth} in order to |
564 You might have to adjust the @{ML_ind default_print_depth} in order to |
565 see the complete list. |
565 see the complete list. |
566 |
566 |
567 The parser @{ML_ind "$$$" in Parse} parses a single keyword. For example: |
567 The parser @{ML_ind "$$$" in Parse} parses a single keyword. For example: |
568 |
568 |
569 @{ML_response [display,gray] |
569 @{ML_response [display,gray] |