diff -r e38885e3ea60 -r ce0112e26b3b src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Mon Aug 15 20:19:41 2011 +0200
+++ b/src/Pure/General/position.ML	Mon Aug 15 20:38:16 2011 +0200
@@ -18,6 +18,7 @@
   val none: T
   val start: T
   val file_name: string -> Properties.T
+  val file_only: string -> T
   val file: string -> T
   val line: int -> T
   val line_file: int -> string -> T
@@ -104,6 +105,7 @@
 fun file_name "" = []
   | file_name name = [(Markup.fileN, name)];
 
+fun file_only name = Pos ((0, 0, 0), file_name name);
 fun file name = Pos ((1, 1, 0), file_name name);
 
 fun line_file i name = Pos ((i, 1, 0), file_name name);