clarified message;
authorwenzelm
Sat Sep 01 17:16:36 2018 +0200 (9 months ago ago)
changeset 688693739acbc2178
parent 68868 5f44ad150ed8
child 68870 53a75627aab7
clarified message;
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Sep 01 16:08:54 2018 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Sep 01 17:16:36 2018 +0200
     1.3 @@ -170,8 +170,7 @@
     1.4    | is_end_theory _ = false;
     1.5  
     1.6  fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
     1.7 -  | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.here pos)
     1.8 -  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.here pos);
     1.9 +  | end_theory pos _ = error ("Malformed theory" ^ Position.here pos);
    1.10  
    1.11  
    1.12  (* presentation context *)
     2.1 --- a/src/Pure/PIDE/document.ML	Sat Sep 01 16:08:54 2018 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Sat Sep 01 17:16:36 2018 +0200
     2.3 @@ -574,9 +574,12 @@
     2.4      val header = read_header node span;
     2.5      val imports = #imports header;
     2.6  
     2.7 -    fun maybe_end_theory pos st =
     2.8 -      SOME (Toplevel.end_theory pos st)
     2.9 -        handle ERROR msg => (Output.error_message msg; NONE);
    2.10 +    fun maybe_eval_result eval = Command.eval_result_state eval
    2.11 +      handle Fail _ => Toplevel.toplevel;
    2.12 +
    2.13 +    fun maybe_end_theory pos st = SOME (Toplevel.end_theory pos st)
    2.14 +      handle ERROR msg => (Output.error_message msg; NONE);
    2.15 +
    2.16      val parents_reports =
    2.17        imports |> map_filter (fn (import, pos) =>
    2.18          (case Thy_Info.lookup_theory import of
    2.19 @@ -584,7 +587,7 @@
    2.20              maybe_end_theory pos
    2.21                (case get_result (snd (the (AList.lookup (op =) deps import))) of
    2.22                  NONE => Toplevel.toplevel
    2.23 -              | SOME (_, eval) => Command.eval_result_state eval)
    2.24 +              | SOME (_, eval) => maybe_eval_result eval)
    2.25          | some => some)
    2.26          |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))));
    2.27