check_goal: produce error instead of warning;
authorwenzelm
Tue Aug 27 11:06:07 2002 +0200 (2002-08-27)
changeset 1352949a0ad8f175e
parent 13528 d14fb18343cb
child 13530 4813fdc0ef17
check_goal: produce error instead of warning;
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Tue Aug 27 11:05:31 2002 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Tue Aug 27 11:06:07 2002 +0200
     1.3 @@ -236,11 +236,9 @@
     1.4  local
     1.5  
     1.6  fun present_thmss kind (thy, named_thmss) =
     1.7 -  let fun present (name, thms) = Present.results (kind ^ "s") name thms in
     1.8 -    if kind = "" orelse kind = Drule.internalK then ()
     1.9 -    else Context.setmp (Some thy) (fn () => seq present named_thmss) ();
    1.10 -    (thy, named_thmss)
    1.11 -  end;
    1.12 + (conditional (kind <> "" andalso kind <> Drule.internalK) (fn () =>
    1.13 +    Context.setmp (Some thy) (Present.results (kind ^ "s")) named_thmss);
    1.14 +  (thy, named_thmss));
    1.15  
    1.16  in
    1.17  
    1.18 @@ -338,19 +336,19 @@
    1.19    | check_goal true state =
    1.20        let
    1.21          val rule = ref (None: thm option);
    1.22 -        fun warn exn =
    1.23 +        fun fail exn =
    1.24            (["Problem! Local statement will fail to solve any pending goal"] @
    1.25            (case exn of None => [] | Some e => [Toplevel.exn_message e]) @
    1.26            (case ! rule of None => [] | Some thm =>
    1.27              [Pretty.string_of (pretty_rule "Failed attempt" (Proof.context_of state) thm)]))
    1.28 -          |> cat_lines |> warning;
    1.29 +          |> cat_lines |> error;
    1.30          val check =
    1.31            (fn () => Seq.pull (SkipProof.local_skip_proof (K (K ()),
    1.32              fn _ => fn thm => rule := Some thm) true state))
    1.33            |> Library.setmp proofs 0
    1.34            |> Library.transform_error;
    1.35          val result = (check (), None) handle Interrupt => raise Interrupt | e => (None, Some e);
    1.36 -      in (case result of (Some _, None) => () | (_, exn) => warn exn); state end;
    1.37 +      in (case result of (Some _, None) => () | (_, exn) => fail exn); state end;
    1.38  
    1.39  end;
    1.40  
    1.41 @@ -469,7 +467,7 @@
    1.42    in
    1.43      if kind = "" orelse kind = Drule.internalK then ()
    1.44      else (print_result (Proof.context_of state) ((kind, name), res);
    1.45 -      Context.setmp (Some thy) Present.multi_result (kind, res));
    1.46 +      Context.setmp (Some thy) (Present.results kind) res);
    1.47      thy
    1.48    end);
    1.49