# HG changeset patch
# User wenzelm
# Date 1184015557 -7200
# Node ID 67c748e5ae54501079b6943cbce437031ac7595c
# Parent  3fd7770f679543437d20aa9e67e1004c1fac7e2c
replaced name by file (unquoted);
str_of: markup;
misc cleanup;

diff -r 3fd7770f6795 -r 67c748e5ae54 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Mon Jul 09 23:12:36 2007 +0200
+++ b/src/Pure/General/position.ML	Mon Jul 09 23:12:37 2007 +0200
@@ -2,54 +2,43 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Input positions.
+Source positions.
 *)
 
 signature POSITION =
 sig
   type T
+  val line_of: T -> int option
+  val file_of: T -> string option
+  val inc: T -> T
   val none: T
   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 file: string -> T
+  val path: Path.T -> T
   val of_properties: Markup.property list -> T
   val properties_of: T -> Markup.property list
+  val str_of: T -> string
 end;
 
 structure Position: POSITION =
 struct
 
-
 (* datatype position *)
 
 datatype T =
   Pos of int option * string option;
 
-val none = Pos (NONE, NONE);
-fun line n = Pos (SOME n, NONE);
-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 *)
+fun file_of (Pos (_, opt_s)) = opt_s;
 
 fun inc (pos as Pos (NONE, _)) = pos
   | inc (Pos (SOME n, opt_s)) = Pos (SOME (n + 1), opt_s);
 
-
-(* str_of *)
+val none = Pos (NONE, NONE);
+fun line n = Pos (SOME n, NONE);
+fun file s = Pos (SOME 1, SOME s);
 
-fun str_of (Pos (NONE, NONE)) = ""
-  | str_of (Pos (SOME n, NONE)) = " (line " ^ string_of_int n ^ ")"
-  | str_of (Pos (NONE, SOME s)) = " (" ^ s ^ ")"
-  | str_of (Pos (SOME n, SOME s)) = " (line " ^ string_of_int n ^ " of " ^ s ^ ")";
+val path = file o Path.implode o Path.expand;
 
 
 (* markup properties *)
@@ -58,14 +47,25 @@
   let
     val lookup = AList.lookup (op =) ps;
     val opt_n =
-      (case lookup Markup.pos_lineN of
+      (case lookup Markup.lineN of
         SOME s => Int.fromString s
       | NONE => NONE);
-    val opt_s = lookup Markup.pos_nameN;
+    val opt_s = lookup Markup.fileN;
   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 => []);
+  (case opt_n of SOME n => [(Markup.lineN, string_of_int n)] | NONE => []) @
+  (case opt_s of SOME s => [(Markup.fileN, s)] | NONE => []);
+
+
+(* str_of *)
+
+fun print (Pos (SOME n, NONE)) = "(line " ^ string_of_int n ^ ")"
+  | print (Pos (NONE, SOME s)) = "(" ^ s ^ ")"
+  | print (Pos (SOME n, SOME s)) = "(line " ^ string_of_int n ^ " of " ^ quote s ^ ")";
+
+fun str_of (Pos (NONE, NONE)) = ""
+  | str_of pos = " " ^ Pretty.string_of (Pretty.markup
+        (Markup.properties (properties_of pos) Markup.position) [Pretty.str (print pos)]);
 
 end;