# HG changeset patch
# User wenzelm
# Date 1310137478 -7200
# Node ID 7270ae921cf28be0add6bd7f68d97c69bb0940b2
# Parent  717e96cf9527e3d926cef22398cfd23f66968f2a
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
Position.offset discriminates postions precisely, now also available for Position.line/line_file;

diff -r 717e96cf9527 -r 7270ae921cf2 src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Fri Jul 08 16:13:34 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Fri Jul 08 17:04:38 2011 +0200
@@ -118,7 +118,7 @@
     val st = (pre, post, Time.fromSeconds (Config.get_global thy timeout))
 
     val str0 = string_of_int o the_default 0
-    val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
+    val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos)
     val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):"
   in
     only_within_range thy pos (apply_actions thy pos name info st) (Actions.get thy)
diff -r 717e96cf9527 -r 7270ae921cf2 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jul 08 16:13:34 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jul 08 17:04:38 2011 +0200
@@ -245,7 +245,7 @@
 fun str_of_pos (pos, triv) =
   let val str0 = string_of_int o the_default 0
   in
-    str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) ^
+    str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos) ^
     (if triv then "[T]" else "")
   end
 
diff -r 717e96cf9527 -r 7270ae921cf2 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jul 08 16:13:34 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jul 08 17:04:38 2011 +0200
@@ -64,8 +64,8 @@
   let
     fun do_line line =
       case line |> space_explode ":" of
-        [line_num, col_num, proof] =>
-        SOME (pairself (the o Int.fromString) (line_num, col_num),
+        [line_num, offset, proof] =>
+        SOME (pairself (the o Int.fromString) (line_num, offset),
               proof |> space_explode " " |> filter_out (curry (op =) ""))
        | _ => NONE
     val proofs = File.read (Path.explode proof_file)
@@ -105,9 +105,9 @@
 fun with_index (i, s) = s ^ "@" ^ string_of_int i
 
 fun action args id ({pre, pos, log, ...} : Mirabelle.run_args) =
-  case (Position.line_of pos, Position.column_of pos) of
-    (SOME line_num, SOME col_num) =>
-    (case Prooftab.lookup (!proof_table) (line_num, col_num) of
+  case (Position.line_of pos, Position.offset_of pos) of
+    (SOME line_num, SOME offset) =>
+    (case Prooftab.lookup (!proof_table) (line_num, offset) of
        SOME proofs =>
        let
          val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre
diff -r 717e96cf9527 -r 7270ae921cf2 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Fri Jul 08 16:13:34 2011 +0200
+++ b/src/Pure/General/markup.ML	Fri Jul 08 17:04:38 2011 +0200
@@ -21,7 +21,6 @@
   val defN: string
   val refN: string
   val lineN: string
-  val columnN: string
   val offsetN: string
   val end_offsetN: string
   val fileN: string
@@ -186,14 +185,13 @@
 (* position *)
 
 val lineN = "line";
-val columnN = "column";
 val offsetN = "offset";
 val end_offsetN = "end_offset";
 val fileN = "file";
 val idN = "id";
 
 val position_properties' = [fileN, idN];
-val position_properties = [lineN, columnN, offsetN, end_offsetN] @ position_properties';
+val position_properties = [lineN, offsetN, end_offsetN] @ position_properties';
 
 val (positionN, position) = markup_elem "position";
 
diff -r 717e96cf9527 -r 7270ae921cf2 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Fri Jul 08 16:13:34 2011 +0200
+++ b/src/Pure/General/markup.scala	Fri Jul 08 17:04:38 2011 +0200
@@ -114,20 +114,18 @@
   /* position */
 
   val LINE = "line"
-  val COLUMN = "column"
   val OFFSET = "offset"
   val END_OFFSET = "end_offset"
   val FILE = "file"
   val ID = "id"
 
   val DEF_LINE = "def_line"
-  val DEF_COLUMN = "def_column"
   val DEF_OFFSET = "def_offset"
   val DEF_END_OFFSET = "def_end_offset"
   val DEF_FILE = "def_file"
   val DEF_ID = "def_id"
 
-  val POSITION_PROPERTIES = Set(LINE, COLUMN, OFFSET, END_OFFSET, FILE, ID)
+  val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
   val POSITION = "position"
 
 
diff -r 717e96cf9527 -r 7270ae921cf2 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');
 
diff -r 717e96cf9527 -r 7270ae921cf2 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Fri Jul 08 16:13:34 2011 +0200
+++ b/src/Pure/General/position.scala	Fri Jul 08 17:04:38 2011 +0200
@@ -39,7 +39,6 @@
 
   private val purge_pos = Map(
     Markup.DEF_LINE -> Markup.LINE,
-    Markup.DEF_COLUMN -> Markup.COLUMN,
     Markup.DEF_OFFSET -> Markup.OFFSET,
     Markup.DEF_END_OFFSET -> Markup.END_OFFSET,
     Markup.DEF_FILE -> Markup.FILE,
diff -r 717e96cf9527 -r 7270ae921cf2 src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Fri Jul 08 16:13:34 2011 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Fri Jul 08 17:04:38 2011 +0200
@@ -18,8 +18,7 @@
         XML.Elem ((e, atts), _) => if e = Markup.positionN then atts else []
       | XML.Text s => Position.file_name s);
   in
-    Position.make
-      {line = line, column = 0, offset = offset, end_offset = end_offset, props = props}
+    Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
   end;
 
 fun exn_position exn =
diff -r 717e96cf9527 -r 7270ae921cf2 src/Pure/ProofGeneral/pgip_isabelle.ML
--- a/src/Pure/ProofGeneral/pgip_isabelle.ML	Fri Jul 08 16:13:34 2011 +0200
+++ b/src/Pure/ProofGeneral/pgip_isabelle.ML	Fri Jul 08 17:04:38 2011 +0200
@@ -74,7 +74,6 @@
 
 fun location_of_position pos =
     let val line = Position.line_of pos
-        val column = Position.column_of pos
         val (url,descr) =
             (case Position.file_of pos of
                NONE => (NONE, NONE)
@@ -85,7 +84,7 @@
                  else (NONE, SOME fname)
                end);
     in
-        { descr=descr, url=url, line=line, column=column, char=NONE, length=NONE }
+        { descr=descr, url=url, line=line, column=NONE, char=NONE, length=NONE }
     end