added property conversions;
tuned;

--- a/src/Pure/General/position.ML	Sat Jul 07 12:16:14 2007 +0200
+++ b/src/Pure/General/position.ML	Sat Jul 07 12:16:15 2007 +0200
@@ -12,10 +12,12 @@
   val line: int -> T
   val name: string -> T
   val line_name: int -> string -> T
+  val line_of: T -> int option
+  val name_of: T -> string option
   val inc: T -> T
   val str_of: T -> string
-  val line_of: T -> int option
-  val name_of: T -> string option
+  val of_properties: Markup.property list -> T
+  val properties_of: T -> Markup.property list
 end;
 
 structure Position: POSITION =
@@ -32,6 +34,9 @@
 fun name s = Pos (NONE, SOME s);
 fun line_name n s = Pos (SOME n, SOME s);
 
+fun line_of (Pos (opt_n, _)) = opt_n;
+fun name_of (Pos (_, opt_s)) = opt_s;
+
 
 (* increment *)
 
@@ -46,10 +51,21 @@
   | str_of (Pos (NONE, SOME s)) = " (" ^ s ^ ")"
   | str_of (Pos (SOME n, SOME s)) = " (line " ^ string_of_int n ^ " of " ^ s ^ ")";
 
-fun line_of (Pos (SOME n,_)) = SOME n
-  | line_of _ = NONE
+
+(* markup properties *)
 
-fun name_of (Pos (_,SOME s)) = SOME s
-  | name_of _ = NONE
+fun of_properties ps =
+  let
+    val lookup = AList.lookup (op =) ps;
+    val opt_n =
+      (case lookup Markup.pos_lineN of
+        SOME s => Int.fromString s
+      | NONE => NONE);
+    val opt_s = lookup Markup.pos_nameN;
+  in Pos (opt_n, opt_s) end;
+
+fun properties_of (Pos (opt_n, opt_s)) =
+  (case opt_n of SOME n => [(Markup.pos_lineN, string_of_int n)] | NONE => []) @
+  (case opt_s of SOME s => [(Markup.pos_nameN, s)] | NONE => []);
 
 end;