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