src/Pure/PIDE/document.ML
changeset 68869 3739acbc2178
parent 68866 d4681a748873
child 69826 1bea05713dde
     1.1 --- a/src/Pure/PIDE/document.ML	Sat Sep 01 16:08:54 2018 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sat Sep 01 17:16:36 2018 +0200
     1.3 @@ -574,9 +574,12 @@
     1.4      val header = read_header node span;
     1.5      val imports = #imports header;
     1.6  
     1.7 -    fun maybe_end_theory pos st =
     1.8 -      SOME (Toplevel.end_theory pos st)
     1.9 -        handle ERROR msg => (Output.error_message msg; NONE);
    1.10 +    fun maybe_eval_result eval = Command.eval_result_state eval
    1.11 +      handle Fail _ => Toplevel.toplevel;
    1.12 +
    1.13 +    fun maybe_end_theory pos st = SOME (Toplevel.end_theory pos st)
    1.14 +      handle ERROR msg => (Output.error_message msg; NONE);
    1.15 +
    1.16      val parents_reports =
    1.17        imports |> map_filter (fn (import, pos) =>
    1.18          (case Thy_Info.lookup_theory import of
    1.19 @@ -584,7 +587,7 @@
    1.20              maybe_end_theory pos
    1.21                (case get_result (snd (the (AList.lookup (op =) deps import))) of
    1.22                  NONE => Toplevel.toplevel
    1.23 -              | SOME (_, eval) => Command.eval_result_state eval)
    1.24 +              | SOME (_, eval) => maybe_eval_result eval)
    1.25          | some => some)
    1.26          |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))));
    1.27