equal
deleted
inserted
replaced
497 |
497 |
498 val scan_verbatim = |
498 val scan_verbatim = |
499 Scan.ahead ($$ "{" -- $$ "*") |-- |
499 Scan.ahead ($$ "{" -- $$ "*") |-- |
500 !!! "unclosed verbatim text" |
500 !!! "unclosed verbatim text" |
501 ((Symbol_Pos.scan_pos --| $$ "{" --| $$ "*") -- |
501 ((Symbol_Pos.scan_pos --| $$ "{" --| $$ "*") -- |
502 Symbol_Pos.change_prompt |
502 ((Scan.repeat scan_verb >> flat) -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos))); |
503 ((Scan.repeat scan_verb >> flat) -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos))); |
|
504 |
503 |
505 val recover_verbatim = |
504 val recover_verbatim = |
506 $$$ "{" @@@ $$$ "*" @@@ (Scan.repeat scan_verb >> flat); |
505 $$$ "{" @@@ $$$ "*" @@@ (Scan.repeat scan_verb >> flat); |
507 |
506 |
508 |
507 |