# HG changeset patch
# User wenzelm
# Date 1294601447 -3600
# Node ID 51310e1ccd6f4f9464c5ce08b75948622369aa3d
# Parent  4a8431c73cf231eb7eed5f6db275abc56792c0fd
more direct treatment of Position.end_offset;
tuned;

diff -r 4a8431c73cf2 -r 51310e1ccd6f src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sun Jan 09 16:03:56 2011 +0100
+++ b/src/Pure/General/markup.ML	Sun Jan 09 20:30:47 2011 +0100
@@ -189,8 +189,8 @@
 val fileN = "file";
 val idN = "id";
 
-val position_properties' = [end_offsetN, fileN, idN];
-val position_properties = [lineN, columnN, offsetN] @ position_properties';
+val position_properties' = [fileN, idN];
+val position_properties = [lineN, columnN, offsetN, end_offsetN] @ position_properties';
 
 val (positionN, position) = markup_elem "position";
 
diff -r 4a8431c73cf2 -r 51310e1ccd6f src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Sun Jan 09 16:03:56 2011 +0100
+++ b/src/Pure/General/position.ML	Sun Jan 09 20:30:47 2011 +0100
@@ -6,11 +6,13 @@
 
 signature POSITION =
 sig
-  type T
-  val value: string -> int -> Properties.T
+  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 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
   val advance: Symbol.symbol -> T -> T
   val distance_of: T -> T -> int
@@ -34,7 +36,7 @@
   val str_of: T -> string
   type range = T * T
   val no_range: range
-  val encode_range: range -> T
+  val set_range: range -> T
   val reset_range: T -> T
   val range: T -> T -> range
   val thread_data: unit -> T
@@ -47,32 +49,41 @@
 
 (* datatype position *)
 
-datatype T = Pos of (int * int * int) * Properties.T;
+datatype T = Pos of (int * 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 valid (i: int) = i > 0;
 fun if_valid i i' = if valid i then i' else i;
 
-fun value k i = if valid i then [(k, string_of_int i)] else [];
-
 
 (* 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 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 file_of (Pos (_, props)) = Properties.get props Markup.fileN;
 
 
 (* advance *)
 
-fun advance_count "\n" (i: int, j: int, k: int) =
-      (if_valid i (i + 1), if_valid j 1, if_valid k (k + 1))
-  | advance_count s (i, j, k) =
-      if Symbol.is_regular s then (i, if_valid j (j + 1), if_valid k (k + 1))
-      else (i, j, k);
+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 invalid_count (i, j, k) =
+fun invalid_count (i, j, k, _: int) =
   not (valid i orelse valid j orelse valid k);
 
 fun advance sym (pos as (Pos (count, props))) =
@@ -81,7 +92,7 @@
 
 (* distance of adjacent positions *)
 
-fun distance_of (Pos ((_, j, k), _)) (Pos ((_, j', k'), _)) =
+fun distance_of (Pos ((_, j, k, _), _)) (Pos ((_, j', k', _), _)) =
   if valid j andalso valid j' then j' - j
   else if valid k andalso valid k' then k' - k
   else 0;
@@ -89,20 +100,20 @@
 
 (* make position *)
 
-val none = Pos ((0, 0, 0), []);
-val start = Pos ((1, 1, 1), []);
+val none = Pos ((0, 0, 0, 0), []);
+val start = Pos ((1, 1, 1, 0), []);
 
 
 fun file_name "" = []
   | file_name name = [(Markup.fileN, name)];
 
-fun file name = Pos ((1, 1, 1), file_name name);
+fun file name = Pos ((1, 1, 1, 0), file_name name);
 
-fun line_file i name = Pos ((i, 0, 0), file_name name);
+fun line_file i name = Pos ((i, 0, 0, 0), file_name name);
 fun line i = line_file i "";
 
-fun id id = Pos ((0, 0, 1), [(Markup.idN, id)]);
-fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
+fun id id = Pos ((0, 0, 1, 0), [(Markup.idN, id)]);
+fun id_only id = Pos ((0, 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);
@@ -116,12 +127,17 @@
       (case Properties.get props name of
         NONE => 0
       | SOME s => the_default 0 (Int.fromString s));
-    val count = (get Markup.lineN, get Markup.columnN, get Markup.offsetN);
-    fun property name = the_list (find_first (fn (x: string, _) => x = name) props);
-  in Pos (count, maps property Markup.position_properties') end;
+  in
+    make {line = get Markup.lineN, column = get Markup.columnN,
+      offset = get Markup.offsetN, end_offset = get Markup.end_offsetN, props = props}
+  end;
+
 
-fun properties_of (Pos ((i, j, k), props)) =
-  value Markup.lineN i @ value Markup.columnN j @ value Markup.offsetN k @ props;
+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 default_properties default props =
   if exists (member (op =) Markup.position_properties o #1) props then props
@@ -162,15 +178,10 @@
 
 val no_range = (none, none);
 
-fun encode_range (Pos (count, props), Pos ((i, j, k), _)) =
-  let val props' = props |> fold Properties.put (value Markup.end_offsetN k)
-  in Pos (count, props') end;
+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 reset_range (Pos (count, props)) =
-  let val props' = props |> Properties.remove Markup.end_offsetN
-  in Pos (count, props') end;
-
-fun range pos pos' = (encode_range (pos, pos'), pos');
+fun range pos pos' = (set_range (pos, pos'), pos');
 
 
 (* thread data *)
diff -r 4a8431c73cf2 -r 51310e1ccd6f src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Sun Jan 09 16:03:56 2011 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Sun Jan 09 20:30:47 2011 +0100
@@ -235,7 +235,7 @@
 
 fun prepare_span commands span =
   let
-    val range_pos = Position.encode_range (Thy_Syntax.span_range span);
+    val range_pos = Position.set_range (Thy_Syntax.span_range span);
     val toks = Thy_Syntax.span_content span;
     val _ = List.app Thy_Syntax.report_token toks;
   in
diff -r 4a8431c73cf2 -r 51310e1ccd6f src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Sun Jan 09 16:03:56 2011 +0100
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Sun Jan 09 20:30:47 2011 +0100
@@ -13,16 +13,14 @@
   let
     val {file = text, startLine = line, startPosition = offset,
       endLine = _, endPosition = end_offset} = loc;
-    val loc_props =
+    val props =
       (case YXML.parse text of
         XML.Elem ((e, atts), _) => if e = Markup.positionN then atts else []
       | XML.Text s => Position.file_name s);
   in
-    Position.value Markup.lineN line @
-    Position.value Markup.offsetN offset @
-    Position.value Markup.end_offsetN end_offset @
-    loc_props
-  end |> Position.of_properties;
+    Position.make
+      {line = line, column = 0, offset = offset, end_offset = end_offset, props = props}
+  end;
 
 fun offset_position_of loc =
   let val pos = position_of loc
diff -r 4a8431c73cf2 -r 51310e1ccd6f src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Sun Jan 09 16:03:56 2011 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Sun Jan 09 20:30:47 2011 +0100
@@ -153,7 +153,7 @@
   Markup.enclose (kind_markup (span_kind span)) (implode (map present_token (span_content span)));
 
 fun report_span span =
-  Position.report (Position.encode_range (span_range span)) (kind_markup (span_kind span));
+  Position.report (Position.set_range (span_range span)) (kind_markup (span_kind span));
 
 end;