# HG changeset patch
# User wenzelm
# Date 1426511715 -3600
# Node ID 8c56b34a88b019b92ec65adf849e4206fd00ea2b
# Parent  4f0d0e4ad68dfefc0ff63c76f2394a7f40ac48a5
more precises positions;
more permissive imports;

diff -r 4f0d0e4ad68d -r 8c56b34a88b0 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Mar 16 13:32:31 2015 +0100
+++ b/src/Pure/PIDE/document.ML	Mon Mar 16 14:15:15 2015 +0100
@@ -520,16 +520,24 @@
     val master_dir = master_directory node;
     val header = read_header node span;
     val imports = #imports header;
-    val parents =
-      imports |> map (fn (import, _) =>
+
+    fun maybe_end_theory pos st =
+      SOME (Toplevel.end_theory pos st)
+        handle ERROR msg => (Output.error_message msg; NONE);
+    val parents_reports =
+      imports |> map_filter (fn (import, pos) =>
         (case loaded_theory import of
-          SOME thy => thy
-        | NONE =>
-            Toplevel.end_theory (Position.file_only import)
+          NONE =>
+            maybe_end_theory pos
               (case get_result (snd (the (AList.lookup (op =) deps import))) of
                 NONE => Toplevel.toplevel
-              | SOME eval => Command.eval_result_state eval)));
-    val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
+              | SOME eval => Command.eval_result_state eval)
+        | some => some)
+        |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))));
+
+    val parents =
+      if null parents_reports then [Thy_Info.get_theory "Pure"] else map #1 parents_reports;
+    val _ = Position.reports (map #2 parents_reports);
   in Resources.begin_theory master_dir header parents end;
 
 fun check_theory full name node =