equal
deleted
inserted
replaced
35 | antiquote_range (Control {range, ...}) = range |
35 | antiquote_range (Control {range, ...}) = range |
36 | antiquote_range (Antiq {range, ...}) = range; |
36 | antiquote_range (Antiq {range, ...}) = range; |
37 |
37 |
38 fun range ants = |
38 fun range ants = |
39 if null ants then Position.no_range |
39 if null ants then Position.no_range |
40 else Position.range (#1 (antiquote_range (hd ants))) (#2 (antiquote_range (List.last ants))); |
40 else Position.range (#1 (antiquote_range (hd ants)), #2 (antiquote_range (List.last ants))); |
41 |
41 |
42 |
42 |
43 (* split lines *) |
43 (* split lines *) |
44 |
44 |
45 fun split_lines input = |
45 fun split_lines input = |
108 val scan_antiq = |
108 val scan_antiq = |
109 Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.scan_pos -- |
109 Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.scan_pos -- |
110 Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace") |
110 Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace") |
111 (Scan.repeats scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >> |
111 (Scan.repeats scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >> |
112 (fn (pos1, (pos2, ((body, pos3), pos4))) => |
112 (fn (pos1, (pos2, ((body, pos3), pos4))) => |
113 {start = Position.set_range (pos1, pos2), |
113 {start = Position.range_position (pos1, pos2), |
114 stop = Position.set_range (pos3, pos4), |
114 stop = Position.range_position (pos3, pos4), |
115 range = Position.range pos1 pos4, |
115 range = Position.range (pos1, pos4), |
116 body = body}); |
116 body = body}); |
117 |
117 |
118 val scan_antiquote = |
118 val scan_antiquote = |
119 scan_txt >> Text || scan_control >> Control || scan_antiq >> Antiq; |
119 scan_txt >> Text || scan_control >> Control || scan_antiq >> Antiq; |
120 |
120 |