75 local |
75 local |
76 |
76 |
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.repeat1 |
80 Scan.repeats1 |
81 (Scan.many1 (fn (s, _) => not (Symbol.is_control s) andalso s <> "@" andalso Symbol.not_eof s) || |
81 (Scan.many1 (fn (s, _) => not (Symbol.is_control s) andalso s <> "@" andalso Symbol.not_eof s) || |
82 Scan.one (fn (s, _) => Symbol.is_control s) --| Scan.ahead (~$$ "\\<open>") >> single || |
82 Scan.one (fn (s, _) => Symbol.is_control s) --| Scan.ahead (~$$ "\\<open>") >> single || |
83 $$$ "@" --| Scan.ahead (~$$ "{")) >> flat; |
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 Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2 || |
87 Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2 || |
88 Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single; |
88 Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single; |
99 in {name = (name, pos), range = range, body = body} end); |
99 in {name = (name, pos), range = range, body = body} end); |
100 |
100 |
101 val scan_antiq = |
101 val scan_antiq = |
102 Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.scan_pos -- |
102 Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.scan_pos -- |
103 Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace") |
103 Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace") |
104 (Scan.repeat scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >> |
104 (Scan.repeats scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >> |
105 (fn (pos1, (pos2, ((body, pos3), pos4))) => |
105 (fn (pos1, (pos2, ((body, pos3), pos4))) => |
106 {start = Position.set_range (pos1, pos2), |
106 {start = Position.set_range (pos1, pos2), |
107 stop = Position.set_range (pos3, pos4), |
107 stop = Position.set_range (pos3, pos4), |
108 range = Position.range pos1 pos4, |
108 range = Position.range pos1 pos4, |
109 body = flat body}); |
109 body = body}); |
110 |
110 |
111 val scan_antiquote = |
111 val scan_antiquote = |
112 scan_control >> Control || scan_antiq >> Antiq || scan_txt >> Text; |
112 scan_control >> Control || scan_antiq >> Antiq || scan_txt >> Text; |
113 |
113 |
114 end; |
114 end; |