tuned error message;

--- 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);

--- a/src/Pure/General/secure.ML	Mon Aug 15 20:19:41 2011 +0200
+++ b/src/Pure/General/secure.ML	Mon Aug 15 20:38:16 2011 +0200
@@ -63,7 +63,7 @@
 val use_file = Secure.use_file;
 
 fun use s =
-  Position.setmp_thread_data (Position.of_properties (Position.file_name s))
+  Position.setmp_thread_data (Position.file_only s)
     (fn () =>
       Secure.use_file ML_Parse.global_context true s
         handle ERROR msg => (writeln msg; error "ML error")) ();

--- a/src/Pure/Isar/toplevel.ML	Mon Aug 15 20:19:41 2011 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Aug 15 20:38:16 2011 +0200
@@ -185,8 +185,8 @@
   | _ => raise UNDEF);
 
 fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
-  | end_theory pos (State (NONE, _)) = error ("Missing theory " ^ Position.str_of pos)
-  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory " ^ Position.str_of pos);
+  | end_theory pos (State (NONE, _)) = error ("Missing theory" ^ Position.str_of pos)
+  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.str_of pos);
 
 
 (* print state *)

--- a/src/Pure/PIDE/document.ML	Mon Aug 15 20:19:41 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Aug 15 20:38:16 2011 +0200
@@ -78,7 +78,7 @@
 fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
 fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
 
-fun get_theory (Node {result, ...}) = Toplevel.end_theory Position.none (Lazy.get_finished result);
+fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.get_finished result);
 fun set_result result = map_node (fn (header, entries, _) => (header, entries, result));
 
 val empty_exec = Lazy.value Toplevel.toplevel;
@@ -347,7 +347,8 @@
                     val parents =
                       imports |> map (fn import =>
                         (case AList.lookup (op =) deps import of
-                          SOME (_, parent_node) => get_theory parent_node
+                          SOME (_, parent_node) =>
+                            get_theory (Position.file_only (import ^ ".thy")) parent_node
                         | NONE => Thy_Info.get_theory (Thy_Info.base_name import)));
                   in Thy_Load.begin_theory dir thy_name imports files parents end
                 fun get_command id =