45 structure Position: POSITION = |
47 structure Position: POSITION = |
46 struct |
48 struct |
47 |
49 |
48 (* datatype position *) |
50 (* datatype position *) |
49 |
51 |
50 datatype T = Pos of (int * int * int) * Properties.T; |
52 datatype T = Pos of (int * int * int * int) * Properties.T; |
|
53 |
|
54 fun norm_props (props: Properties.T) = |
|
55 maps (fn a => the_list (find_first (fn (b, _) => a = b) props)) Markup.position_properties'; |
|
56 |
|
57 fun make {line = i, column = j, offset = k, end_offset = l, props} = |
|
58 Pos ((i, j, k, l), norm_props props); |
|
59 |
|
60 fun dest (Pos ((i, j, k, l), props)) = |
|
61 {line = i, column = j, offset = k, end_offset = l, props = props}; |
|
62 |
51 |
63 |
52 fun valid (i: int) = i > 0; |
64 fun valid (i: int) = i > 0; |
53 fun if_valid i i' = if valid i then i' else i; |
65 fun if_valid i i' = if valid i then i' else i; |
54 |
66 |
55 fun value k i = if valid i then [(k, string_of_int i)] else []; |
|
56 |
|
57 |
67 |
58 (* fields *) |
68 (* fields *) |
59 |
69 |
60 fun line_of (Pos ((i, _, _), _)) = if valid i then SOME i else NONE; |
70 fun line_of (Pos ((i, _, _, _), _)) = if valid i then SOME i else NONE; |
61 fun column_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE; |
71 fun column_of (Pos ((_, j, _, _), _)) = if valid j then SOME j else NONE; |
62 fun offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE; |
72 fun offset_of (Pos ((_, _, k, _), _)) = if valid k then SOME k else NONE; |
|
73 fun end_offset_of (Pos ((_, _, _, l), _)) = if valid l then SOME l else NONE; |
63 |
74 |
64 fun file_of (Pos (_, props)) = Properties.get props Markup.fileN; |
75 fun file_of (Pos (_, props)) = Properties.get props Markup.fileN; |
65 |
76 |
66 |
77 |
67 (* advance *) |
78 (* advance *) |
68 |
79 |
69 fun advance_count "\n" (i: int, j: int, k: int) = |
80 fun advance_count "\n" (i: int, j: int, k: int, l: int) = |
70 (if_valid i (i + 1), if_valid j 1, if_valid k (k + 1)) |
81 (if_valid i (i + 1), if_valid j 1, if_valid k (k + 1), l) |
71 | advance_count s (i, j, k) = |
82 | advance_count s (i, j, k, l) = |
72 if Symbol.is_regular s then (i, if_valid j (j + 1), if_valid k (k + 1)) |
83 if Symbol.is_regular s then (i, if_valid j (j + 1), if_valid k (k + 1), l) |
73 else (i, j, k); |
84 else (i, j, k, l); |
74 |
85 |
75 fun invalid_count (i, j, k) = |
86 fun invalid_count (i, j, k, _: int) = |
76 not (valid i orelse valid j orelse valid k); |
87 not (valid i orelse valid j orelse valid k); |
77 |
88 |
78 fun advance sym (pos as (Pos (count, props))) = |
89 fun advance sym (pos as (Pos (count, props))) = |
79 if invalid_count count then pos else Pos (advance_count sym count, props); |
90 if invalid_count count then pos else Pos (advance_count sym count, props); |
80 |
91 |
81 |
92 |
82 (* distance of adjacent positions *) |
93 (* distance of adjacent positions *) |
83 |
94 |
84 fun distance_of (Pos ((_, j, k), _)) (Pos ((_, j', k'), _)) = |
95 fun distance_of (Pos ((_, j, k, _), _)) (Pos ((_, j', k', _), _)) = |
85 if valid j andalso valid j' then j' - j |
96 if valid j andalso valid j' then j' - j |
86 else if valid k andalso valid k' then k' - k |
97 else if valid k andalso valid k' then k' - k |
87 else 0; |
98 else 0; |
88 |
99 |
89 |
100 |
90 (* make position *) |
101 (* make position *) |
91 |
102 |
92 val none = Pos ((0, 0, 0), []); |
103 val none = Pos ((0, 0, 0, 0), []); |
93 val start = Pos ((1, 1, 1), []); |
104 val start = Pos ((1, 1, 1, 0), []); |
94 |
105 |
95 |
106 |
96 fun file_name "" = [] |
107 fun file_name "" = [] |
97 | file_name name = [(Markup.fileN, name)]; |
108 | file_name name = [(Markup.fileN, name)]; |
98 |
109 |
99 fun file name = Pos ((1, 1, 1), file_name name); |
110 fun file name = Pos ((1, 1, 1, 0), file_name name); |
100 |
111 |
101 fun line_file i name = Pos ((i, 0, 0), file_name name); |
112 fun line_file i name = Pos ((i, 0, 0, 0), file_name name); |
102 fun line i = line_file i ""; |
113 fun line i = line_file i ""; |
103 |
114 |
104 fun id id = Pos ((0, 0, 1), [(Markup.idN, id)]); |
115 fun id id = Pos ((0, 0, 1, 0), [(Markup.idN, id)]); |
105 fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]); |
116 fun id_only id = Pos ((0, 0, 0, 0), [(Markup.idN, id)]); |
106 |
117 |
107 fun get_id (Pos (_, props)) = Properties.get props Markup.idN; |
118 fun get_id (Pos (_, props)) = Properties.get props Markup.idN; |
108 fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props); |
119 fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props); |
109 |
120 |
110 |
121 |
114 let |
125 let |
115 fun get name = |
126 fun get name = |
116 (case Properties.get props name of |
127 (case Properties.get props name of |
117 NONE => 0 |
128 NONE => 0 |
118 | SOME s => the_default 0 (Int.fromString s)); |
129 | SOME s => the_default 0 (Int.fromString s)); |
119 val count = (get Markup.lineN, get Markup.columnN, get Markup.offsetN); |
130 in |
120 fun property name = the_list (find_first (fn (x: string, _) => x = name) props); |
131 make {line = get Markup.lineN, column = get Markup.columnN, |
121 in Pos (count, maps property Markup.position_properties') end; |
132 offset = get Markup.offsetN, end_offset = get Markup.end_offsetN, props = props} |
122 |
133 end; |
123 fun properties_of (Pos ((i, j, k), props)) = |
134 |
124 value Markup.lineN i @ value Markup.columnN j @ value Markup.offsetN k @ props; |
135 |
|
136 fun value k i = if valid i then [(k, string_of_int i)] else []; |
|
137 |
|
138 fun properties_of (Pos ((i, j, k, l), props)) = |
|
139 value Markup.lineN i @ value Markup.columnN j @ |
|
140 value Markup.offsetN k @ value Markup.end_offsetN l @ props; |
125 |
141 |
126 fun default_properties default props = |
142 fun default_properties default props = |
127 if exists (member (op =) Markup.position_properties o #1) props then props |
143 if exists (member (op =) Markup.position_properties o #1) props then props |
128 else properties_of default @ props; |
144 else properties_of default @ props; |
129 |
145 |
160 |
176 |
161 type range = T * T; |
177 type range = T * T; |
162 |
178 |
163 val no_range = (none, none); |
179 val no_range = (none, none); |
164 |
180 |
165 fun encode_range (Pos (count, props), Pos ((i, j, k), _)) = |
181 fun set_range (Pos ((i, j, k, _), props), Pos ((_, _, k', _), _)) = Pos ((i, j, k, k'), props); |
166 let val props' = props |> fold Properties.put (value Markup.end_offsetN k) |
182 fun reset_range (Pos ((i, j, k, _), props)) = Pos ((i, j, k, 0), props); |
167 in Pos (count, props') end; |
183 |
168 |
184 fun range pos pos' = (set_range (pos, pos'), pos'); |
169 fun reset_range (Pos (count, props)) = |
|
170 let val props' = props |> Properties.remove Markup.end_offsetN |
|
171 in Pos (count, props') end; |
|
172 |
|
173 fun range pos pos' = (encode_range (pos, pos'), pos'); |
|
174 |
185 |
175 |
186 |
176 (* thread data *) |
187 (* thread data *) |
177 |
188 |
178 local val tag = Universal.tag () : T Universal.tag in |
189 local val tag = Universal.tag () : T Universal.tag in |