# HG changeset patch # User wenzelm # Date 1364403487 -3600 # Node ID 4e4b56b7a3a531ab463d0c2260b13242f380e5de # Parent 7ada6dfa9ab5118a524551ef4e4a2cfe54d2e907 more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs); diff -r 7ada6dfa9ab5 -r 4e4b56b7a3a5 src/HOL/Library/refute.ML --- a/src/HOL/Library/refute.ML Wed Mar 27 17:55:21 2013 +0100 +++ b/src/HOL/Library/refute.ML Wed Mar 27 17:58:07 2013 +0100 @@ -3202,6 +3202,7 @@ "try to find a model that refutes a given subgoal" (scan_parms -- Scan.optional Parse.nat 1 >> (fn (parms, i) => + Toplevel.unknown_proof o Toplevel.keep (fn state => let val ctxt = Toplevel.context_of state; diff -r 7ada6dfa9ab5 -r 4e4b56b7a3a5 src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Mar 27 17:55:21 2013 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Mar 27 17:58:07 2013 +0100 @@ -368,11 +368,6 @@ in if blocking then go () else Future.fork (tap go) |> K (unknownN, state) end |> `(fn (outcome_code, _) => outcome_code = genuineN) -fun nitpick_trans (params, i) = - Toplevel.keep (fn state => - pick_nits params Normal i (Toplevel.proof_position_of state) - (Toplevel.proof_of state) |> K ()) - fun string_for_raw_param (name, value) = name ^ " = " ^ stringify_raw_param_value value @@ -391,7 +386,11 @@ val _ = Outer_Syntax.improper_command @{command_spec "nitpick"} "try to find a counterexample for a given subgoal using Nitpick" - ((parse_params -- Scan.optional Parse.nat 1) #>> nitpick_trans) + (parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) => + Toplevel.unknown_proof o + Toplevel.keep (fn state => + ignore (pick_nits params Normal i (Toplevel.proof_position_of state) + (Toplevel.proof_of state))))) val _ = Outer_Syntax.command @{command_spec "nitpick_params"} diff -r 7ada6dfa9ab5 -r 4e4b56b7a3a5 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Mar 27 17:55:21 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Mar 27 17:58:07 2013 +0100 @@ -419,6 +419,7 @@ end fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) = + Toplevel.unknown_proof o Toplevel.keep (hammer_away params subcommand opt_i fact_override o Toplevel.proof_of) diff -r 7ada6dfa9ab5 -r 4e4b56b7a3a5 src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Wed Mar 27 17:55:21 2013 +0100 +++ b/src/HOL/Tools/try0.ML Wed Mar 27 17:58:07 2013 +0100 @@ -156,6 +156,7 @@ fun try0 timeout_opt = fst oo do_try0 Normal timeout_opt fun try0_trans quad = + Toplevel.unknown_proof o Toplevel.keep (K () o do_try0 Normal (SOME default_timeout) quad o Toplevel.proof_of) diff -r 7ada6dfa9ab5 -r 4e4b56b7a3a5 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Wed Mar 27 17:55:21 2013 +0100 +++ b/src/Tools/quickcheck.ML Wed Mar 27 17:58:07 2013 +0100 @@ -532,8 +532,8 @@ val _ = Outer_Syntax.improper_command @{command_spec "quickcheck"} "try to find counterexample for subgoal" - (parse_args -- Scan.optional Parse.nat 1 - >> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i))); + (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) => + Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i))); (* automatic testing *) diff -r 7ada6dfa9ab5 -r 4e4b56b7a3a5 src/Tools/solve_direct.ML --- a/src/Tools/solve_direct.ML Wed Mar 27 17:55:21 2013 +0100 +++ b/src/Tools/solve_direct.ML Wed Mar 27 17:58:07 2013 +0100 @@ -109,7 +109,8 @@ val _ = Outer_Syntax.improper_command @{command_spec "solve_direct"} "try to solve conjectures directly with existing theorems" - (Scan.succeed (Toplevel.keep (ignore o solve_direct o Toplevel.proof_of))); + (Scan.succeed (Toplevel.unknown_proof o + Toplevel.keep (ignore o solve_direct o Toplevel.proof_of))); (* hook *) diff -r 7ada6dfa9ab5 -r 4e4b56b7a3a5 src/Tools/try.ML --- a/src/Tools/try.ML Wed Mar 27 17:55:21 2013 +0100 +++ b/src/Tools/try.ML Wed Mar 27 17:58:07 2013 +0100 @@ -90,7 +90,7 @@ val _ = Outer_Syntax.improper_command @{command_spec "try"} "try a combination of automatic proving and disproving tools" - (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of))) + (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of))) (* automatic try *)