src/Pure/General/position.ML

--- 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');