# HG changeset patch
# User wenzelm
# Date 1535814996 -7200
# Node ID 3739acbc2178ee51ef0d36563e7c6ba4c5fd00ec
# Parent  5f44ad150ed8f1b895bcd391325898054bcd2bf4
clarified message;

diff -r 5f44ad150ed8 -r 3739acbc2178 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Sep 01 16:08:54 2018 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat Sep 01 17:16:36 2018 +0200
@@ -170,8 +170,7 @@
   | is_end_theory _ = false;
 
 fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
-  | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.here pos)
-  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.here pos);
+  | end_theory pos _ = error ("Malformed theory" ^ Position.here pos);
 
 
 (* presentation context *)
diff -r 5f44ad150ed8 -r 3739acbc2178 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sat Sep 01 16:08:54 2018 +0200
+++ b/src/Pure/PIDE/document.ML	Sat Sep 01 17:16:36 2018 +0200
@@ -574,9 +574,12 @@
     val header = read_header node span;
     val imports = #imports header;
 
-    fun maybe_end_theory pos st =
-      SOME (Toplevel.end_theory pos st)
-        handle ERROR msg => (Output.error_message msg; NONE);
+    fun maybe_eval_result eval = Command.eval_result_state eval
+      handle Fail _ => Toplevel.toplevel;
+
+    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 Thy_Info.lookup_theory import of
@@ -584,7 +587,7 @@
             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)
+              | SOME (_, eval) => maybe_eval_result eval)
         | some => some)
         |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))));