--- a/src/Pure/General/position.ML Fri Jul 08 16:13:34 2011 +0200
+++ b/src/Pure/General/position.ML Fri Jul 08 17:04:38 2011 +0200
@@ -7,10 +7,9 @@
signature POSITION =
sig
eqtype T
- val make: {line: int, column: int, offset: int, end_offset: int, props: Properties.T} -> T
- val dest: T -> {line: int, column: int, offset: int, end_offset: int, props: Properties.T}
+ val make: {line: int, offset: int, end_offset: int, props: Properties.T} -> T
+ val dest: T -> {line: int, offset: int, end_offset: int, props: Properties.T}
val line_of: T -> int option
- val column_of: T -> int option
val offset_of: T -> int option
val end_offset_of: T -> int option
val file_of: T -> string option
@@ -53,17 +52,13 @@
(* datatype position *)
-datatype T = Pos of (int * int * int * int) * Properties.T;
+datatype T = Pos of (int * int * int) * Properties.T;
fun norm_props (props: Properties.T) =
maps (fn a => the_list (find_first (fn (b, _) => a = b) props)) Markup.position_properties';
-fun make {line = i, column = j, offset = k, end_offset = l, props} =
- Pos ((i, j, k, l), norm_props props);
-
-fun dest (Pos ((i, j, k, l), props)) =
- {line = i, column = j, offset = k, end_offset = l, props = props};
-
+fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props);
+fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};
fun valid (i: int) = i > 0;
fun if_valid i i' = if valid i then i' else i;
@@ -71,24 +66,23 @@
(* fields *)
-fun line_of (Pos ((i, _, _, _), _)) = if valid i then SOME i else NONE;
-fun column_of (Pos ((_, j, _, _), _)) = if valid j then SOME j else NONE;
-fun offset_of (Pos ((_, _, k, _), _)) = if valid k then SOME k else NONE;
-fun end_offset_of (Pos ((_, _, _, l), _)) = if valid l then SOME l else NONE;
+fun line_of (Pos ((i, _, _), _)) = if valid i then SOME i else NONE;
+fun offset_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE;
+fun end_offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE;
fun file_of (Pos (_, props)) = Properties.get props Markup.fileN;
(* advance *)
-fun advance_count "\n" (i: int, j: int, k: int, l: int) =
- (if_valid i (i + 1), if_valid j 1, if_valid k (k + 1), l)
- | advance_count s (i, j, k, l) =
- if Symbol.is_regular s then (i, if_valid j (j + 1), if_valid k (k + 1), l)
- else (i, j, k, l);
+fun advance_count "\n" (i: int, j: int, k: int) =
+ (if_valid i (i + 1), if_valid j (j + 1), k)
+ | advance_count s (i, j, k) =
+ if Symbol.is_regular s then (i, if_valid j (j + 1), k)
+ else (i, j, k);
-fun invalid_count (i, j, k, _: int) =
- not (valid i orelse valid j orelse valid k);
+fun invalid_count (i, j, _: int) =
+ not (valid i orelse valid j);
fun advance sym (pos as (Pos (count, props))) =
if invalid_count count then pos else Pos (advance_count sym count, props);
@@ -96,28 +90,27 @@
(* distance of adjacent positions *)
-fun distance_of (Pos ((_, j, k, _), _)) (Pos ((_, j', k', _), _)) =
+fun distance_of (Pos ((_, j, _), _)) (Pos ((_, j', _), _)) =
if valid j andalso valid j' then j' - j
- else if valid k andalso valid k' then k' - k
else 0;
(* make position *)
-val none = Pos ((0, 0, 0, 0), []);
-val start = Pos ((1, 1, 1, 0), []);
+val none = Pos ((0, 0, 0), []);
+val start = Pos ((1, 1, 0), []);
fun file_name "" = []
| file_name name = [(Markup.fileN, name)];
-fun file name = Pos ((1, 1, 1, 0), file_name name);
+fun file name = Pos ((1, 1, 0), file_name name);
-fun line_file i name = Pos ((i, 0, 0, 0), file_name name);
+fun line_file i name = Pos ((i, 1, 0), file_name name);
fun line i = line_file i "";
-fun id id = Pos ((0, 0, 1, 0), [(Markup.idN, id)]);
-fun id_only id = Pos ((0, 0, 0, 0), [(Markup.idN, id)]);
+fun id id = Pos ((0, 1, 0), [(Markup.idN, id)]);
+fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
@@ -132,16 +125,15 @@
NONE => 0
| SOME s => the_default 0 (Int.fromString s));
in
- make {line = get Markup.lineN, column = get Markup.columnN,
- offset = get Markup.offsetN, end_offset = get Markup.end_offsetN, props = props}
+ make {line = get Markup.lineN, offset = get Markup.offsetN,
+ end_offset = get Markup.end_offsetN, props = props}
end;
fun value k i = if valid i then [(k, string_of_int i)] else [];
-fun properties_of (Pos ((i, j, k, l), props)) =
- value Markup.lineN i @ value Markup.columnN j @
- value Markup.offsetN k @ value Markup.end_offsetN l @ props;
+fun properties_of (Pos ((i, j, k), props)) =
+ value Markup.lineN i @ value Markup.offsetN j @ value Markup.end_offsetN k @ props;
val def_properties_of = properties_of #> (map (fn (x, y) => ("def_" ^ x, y)));
@@ -191,8 +183,8 @@
val no_range = (none, none);
-fun set_range (Pos ((i, j, k, _), props), Pos ((_, _, k', _), _)) = Pos ((i, j, k, k'), props);
-fun reset_range (Pos ((i, j, k, _), props)) = Pos ((i, j, k, 0), props);
+fun set_range (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props);
+fun reset_range (Pos ((i, j, _), props)) = Pos ((i, j, 0), props);
fun range pos pos' = (set_range (pos, pos'), pos');