1.1 --- a/src/Pure/General/position.ML	Wed May 14 11:05:08 2008 +0200
     1.2 +++ b/src/Pure/General/position.ML	Wed May 14 11:05:10 2008 +0200
     1.3 @@ -12,9 +12,9 @@
     1.4    val column_of: T -> int option
     1.5    val file_of: T -> string option
     1.6    val none: T
     1.7 +  val line_file: int -> string -> T
     1.8    val line: int -> T
     1.9    val file: string -> T
    1.10 -  val path: Path.T -> T
    1.11    val advance: Symbol.symbol -> T -> T
    1.12    val of_properties: Markup.property list -> T
    1.13    val properties_of: T -> Markup.property list
    1.14 @@ -40,10 +40,13 @@
    1.15  
    1.16  fun file_of (Pos (_, props)) = AList.lookup (op =) props Markup.fileN;
    1.17  
    1.18 +
    1.19  val none = Pos (NONE, []);
    1.20 -fun line m = Pos (SOME (m, 1), []);
    1.21 -fun file name = Pos (SOME (1, 1), [(Markup.fileN, name)]);
    1.22 -val path = file o Path.implode o Path.expand;
    1.23 +
    1.24 +fun line_file m name = Pos (SOME (m, 1), if name = "" then [] else [(Markup.fileN, name)]);
    1.25 +fun line m = line_file m "";
    1.26 +val file = line_file 1;
    1.27 +
    1.28  
    1.29  fun advance "\n" (Pos (SOME (m, _), props)) = Pos (SOME (m + 1, 1), props)
    1.30    | advance s (pos as Pos (SOME (m, n), props)) =