improved errors;
authorwenzelm
Tue Jul 06 21:06:03 1999 +0200 (1999-07-06)
changeset 6903682f8a9ec75d
parent 6902 5f126c495771
child 6904 4125d6b6d8f9
improved errors;
src/Pure/Isar/calculation.ML
     1.1 --- a/src/Pure/Isar/calculation.ML	Tue Jul 06 21:04:37 1999 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Tue Jul 06 21:06:03 1999 +0200
     1.3 @@ -120,13 +120,16 @@
     1.4  
     1.5  fun calculate final opt_rules print state =
     1.6    let
     1.7 +    fun err_if b msg = if b then raise Proof.STATE (msg, state) else ();
     1.8      val fact = Proof.the_fact state;
     1.9      val rules = Seq.of_list (case opt_rules of None => get_local_rules state | Some thms => thms);
    1.10 -    val calculations =
    1.11 +    val (initial, calculations) =
    1.12        (case get_calculation state of
    1.13 -        None => Seq.single fact
    1.14 -      | Some thm => Seq.flat (Seq.map (Method.multi_resolve [thm, fact]) rules));
    1.15 +        None => (true, Seq.single fact)
    1.16 +      | Some thm => (false, Seq.flat (Seq.map (Method.multi_resolve [thm, fact]) rules)));
    1.17    in
    1.18 +    err_if (initial andalso final) "No calculation yet";
    1.19 +    err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
    1.20      calculations |> Seq.map (fn calc =>
    1.21        (print calc;
    1.22          (if final then