equal
deleted
inserted
replaced
77 val err_prefix = "Antiquotation lexical error: "; |
77 val err_prefix = "Antiquotation lexical error: "; |
78 |
78 |
79 val scan_txt = |
79 val scan_txt = |
80 Scan.repeats1 |
80 Scan.repeats1 |
81 (Scan.many1 (fn (s, _) => |
81 (Scan.many1 (fn (s, _) => |
82 not (Symbol.is_control s) andalso s <> "\\<open>" andalso s <> "@" andalso Symbol.not_eof s) || |
82 not (Symbol.is_control s) andalso s <> Symbol.open_ andalso s <> "@" andalso Symbol.not_eof s) || |
83 $$$ "@" --| Scan.ahead (~$$ "{")); |
83 $$$ "@" --| Scan.ahead (~$$ "{")); |
84 |
84 |
85 val scan_antiq_body = |
85 val scan_antiq_body = |
86 Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 || |
86 Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 || |
87 Symbol_Pos.scan_cartouche err_prefix || |
87 Symbol_Pos.scan_cartouche err_prefix || |