equal
deleted
inserted
replaced
81 |
81 |
82 in |
82 in |
83 |
83 |
84 val scan_antiq = |
84 val scan_antiq = |
85 Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |-- |
85 Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |-- |
86 Symbol_Pos.!!! "missing closing brace of antiquotation" |
86 Symbol_Pos.!!! (fn () => "missing closing brace of antiquotation") |
87 (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos))) |
87 (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos))) |
88 >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2)); |
88 >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2)); |
89 |
89 |
90 fun scan x = (scan_antiq >> Antiq || scan_open >> Open || scan_close >> Close) x; |
90 fun scan x = (scan_antiq >> Antiq || scan_open >> Open || scan_close >> Close) x; |
91 val scan_text = scan || Scan.repeat1 scan_txt >> (Text o flat); |
91 val scan_text = scan || Scan.repeat1 scan_txt >> (Text o flat); |