# HG changeset patch
# User wenzelm
# Date 1210755910 -7200
# Node ID 9e824d8f4512310a361d9a78c1d71b050c96c069
# Parent  bb68f50644a9f1f5c583aad55b68e54efe1dd7c8
renamed Position.path to Path.position;
added line_file, ignore empty name;

diff -r bb68f50644a9 -r 9e824d8f4512 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Wed May 14 11:05:08 2008 +0200
+++ b/src/Pure/General/position.ML	Wed May 14 11:05:10 2008 +0200
@@ -12,9 +12,9 @@
   val column_of: T -> int option
   val file_of: T -> string option
   val none: T
+  val line_file: int -> string -> 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
@@ -40,10 +40,13 @@
 
 fun file_of (Pos (_, props)) = AList.lookup (op =) props Markup.fileN;
 
+
 val none = Pos (NONE, []);
-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;
+
+fun line_file m name = Pos (SOME (m, 1), if name = "" then [] else [(Markup.fileN, name)]);
+fun line m = line_file m "";
+val file = line_file 1;
+
 
 fun advance "\n" (Pos (SOME (m, _), props)) = Pos (SOME (m + 1, 1), props)
   | advance s (pos as Pos (SOME (m, n), props)) =