equal
deleted
inserted
replaced
142 |
142 |
143 (* scan verbatim text *) |
143 (* scan verbatim text *) |
144 |
144 |
145 val scan_verb = |
145 val scan_verb = |
146 scan_blank || |
146 scan_blank || |
147 keep_line ($$ "|" --| Scan.ahead (Scan.one (not_equal "}"))) || |
147 keep_line ($$ "*" --| Scan.ahead (Scan.one (not_equal "}"))) || |
148 keep_line (Scan.one (not_equal "|" andf Symbol.not_eof)); |
148 keep_line (Scan.one (not_equal "*" andf Symbol.not_eof)); |
149 |
149 |
150 val scan_verbatim = |
150 val scan_verbatim = |
151 keep_line ($$ "{" -- $$ "|") |-- |
151 keep_line ($$ "{" -- $$ "*") |-- |
152 !! (lex_err (K "missing end of verbatim text")) |
152 !! (lex_err (K "missing end of verbatim text")) |
153 (change_prompt ((Scan.repeat scan_verb >> implode) --| keep_line ($$ "|" -- $$ "}"))); |
153 (change_prompt ((Scan.repeat scan_verb >> implode) --| keep_line ($$ "*" -- $$ "}"))); |
154 |
154 |
155 |
155 |
156 (* scan space *) |
156 (* scan space *) |
157 |
157 |
158 val is_space = Symbol.is_blank andf not_equal "\n"; |
158 val is_space = Symbol.is_blank andf not_equal "\n"; |