# HG changeset patch
# User wenzelm
# Date 1201555643 -3600
# Node ID 7a8aee8353cfb6ca1ce9023014eafcf1db77d748
# Parent  469ee728a5d77ffa47f6b5f723928650a0853b0e
added column field;
replaced inc by general advance operation;
str_of: no output for file without line information;

diff -r 469ee728a5d7 -r 7a8aee8353cf src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Mon Jan 28 22:27:23 2008 +0100
+++ b/src/Pure/General/position.ML	Mon Jan 28 22:27:23 2008 +0100
@@ -9,18 +9,19 @@
 sig
   type T
   val line_of: T -> int option
+  val column_of: T -> int option
   val file_of: T -> string option
-  val inc: T -> T
   val none: T
   val line: int -> T
   val file: string -> T
   val path: Path.T -> T
+  val advance: Symbol.symbol -> T -> T
   val of_properties: Markup.property list -> T
   val properties_of: T -> Markup.property list
+  val str_of: T -> string
   val thread_data: unit -> T
   val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
   val setmp_thread_data_seq: T -> ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq
-  val str_of: T -> string
 end;
 
 structure Position: POSITION =
@@ -28,34 +29,63 @@
 
 (* datatype position *)
 
-datatype T = Pos of int option * Markup.property list;
+datatype T = Pos of (int * int) option * Markup.property list;
+
+fun line_of (Pos (SOME (m, _), _)) = SOME m
+  | line_of _ = NONE;
 
-fun line_of (Pos (opt_n, _)) = opt_n;
-fun file_of (Pos (_, props)) = AList.lookup (op =) props Markup.fileN ;
+fun column_of (Pos (SOME (_, n), _)) = SOME n
+  | column_of _ = NONE;
 
-fun inc (pos as Pos (NONE, _)) = pos
-  | inc (Pos (SOME n, props)) = Pos (SOME (n + 1), props);
+fun file_of (Pos (_, props)) = AList.lookup (op =) props Markup.fileN;
 
 val none = Pos (NONE, []);
-fun line n = Pos (SOME n, []);
-fun file s = Pos (SOME 1, [(Markup.fileN, s)]);
+fun line m = Pos (SOME (m, 1), []);
+fun file name = Pos (SOME (1, 1), [(Markup.fileN, name)]);
+val path = file o Path.implode o Path.expand;
 
-val path = file o Path.implode o Path.expand;
+fun advance "\n" (Pos (SOME (m, _), props)) = Pos (SOME (m + 1, 1), props)
+  | advance sym (pos as Pos (SOME (m, n), props)) =
+      if Symbol.is_regular sym then Pos (SOME (m, n + 1), props) else pos
+  | advance _ pos = pos;
 
 
 (* markup properties *)
 
+fun get_int props (name: string) =
+  (case AList.lookup (op =) props name of
+    NONE => NONE
+  | SOME s => Int.fromString s);
+
 fun of_properties props =
   let
-    val opt_n =
-      (case AList.lookup (op =) props Markup.lineN of
-        SOME s => Int.fromString s
-      | NONE => NONE);
-    fun get name = the_list (find_first (fn (x: string, _) => x = name) props);
-  in (Pos (opt_n, get Markup.fileN @ get Markup.idN)) end;
+    val count =
+      (case get_int props Markup.lineN of
+        NONE => NONE
+      | SOME m => SOME (m, the_default 1 (get_int props Markup.columnN)));
+    fun property name = the_list (find_first (fn (x: string, _) => x = name) props);
+  in (Pos (count, property Markup.fileN @ property Markup.idN)) end;
+
+fun properties_of (Pos (count, props)) =
+  (case count of
+    NONE => []
+  | SOME (m, n) => [(Markup.lineN, string_of_int m), (Markup.columnN, string_of_int n)]) @ props;
+
 
-fun properties_of (Pos (opt_n, props)) =
-  (case opt_n of SOME n => [(Markup.lineN, string_of_int n)] | NONE => []) @ props;
+(* str_of *)
+
+fun str_of pos =
+  let
+    val props = properties_of pos;
+    val s =
+      (case (line_of pos, file_of pos) of
+        (SOME m, NONE) => "(line " ^ string_of_int m ^ ")"
+      | (SOME m, SOME name) => "(line " ^ string_of_int m ^ " of " ^ quote name ^ ")"
+      | _ => "");
+  in
+    if null props then ""
+    else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s
+  end;
 
 
 (* thread data *)
@@ -70,16 +100,4 @@
 
 end;
 
-
-(* str_of *)
-
-fun print (SOME n, NONE) = "(line " ^ string_of_int n ^ ")"
-  | print (NONE, SOME s) = "(" ^ s ^ ")"
-  | print (SOME n, SOME s) = "(line " ^ string_of_int n ^ " of " ^ quote s ^ ")";
-
-fun str_of pos =
-  (case (line_of pos, file_of pos) of
-    (NONE, NONE) => ""
-  | res => " " ^ Markup.markup (Markup.properties (properties_of pos) Markup.position) (print res));
-
 end;