# HG changeset patch # User wenzelm # Date 1429186712 -7200 # Node ID 96a4765ba7d10abfc93a29dac9f747d282b9de78 # Parent c48d536231fee1d23875619090d25bea9cae1a7f explicit error for Toplevel.proof_of; eliminated obsolete Toplevel.unknown_proof; more total Toplevel.proof_position_of; diff -r c48d536231fe -r 96a4765ba7d1 NEWS --- a/NEWS Thu Apr 16 13:48:10 2015 +0200 +++ b/NEWS Thu Apr 16 14:18:32 2015 +0200 @@ -398,6 +398,9 @@ derivatives) instead, which is not affected by the change. Potential INCOMPATIBILITY in rare applications of Name_Space.intern. +* Subtle change of error semantics of Toplevel.proof_of: regular user +ERROR instead of internal Toplevel.UNDEF. + * Basic combinators map, fold, fold_map, split_list, apply are available as parameterized antiquotations, e.g. @{map 4} for lists of quadruples. diff -r c48d536231fe -r 96a4765ba7d1 src/Doc/Implementation/Integration.thy --- a/src/Doc/Implementation/Integration.thy Thu Apr 16 13:48:10 2015 +0200 +++ b/src/Doc/Implementation/Integration.thy Thu Apr 16 14:18:32 2015 +0200 @@ -62,7 +62,7 @@ for an empty toplevel state. \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof - state if available, otherwise it raises @{ML Toplevel.UNDEF}. + state if available, otherwise it raises an error. \end{description} \ diff -r c48d536231fe -r 96a4765ba7d1 src/HOL/Library/refute.ML --- a/src/HOL/Library/refute.ML Thu Apr 16 13:48:10 2015 +0200 +++ b/src/HOL/Library/refute.ML Thu Apr 16 14:18:32 2015 +0200 @@ -2969,7 +2969,6 @@ "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 c48d536231fe -r 96a4765ba7d1 src/HOL/Tools/Nitpick/nitpick_commands.ML --- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Thu Apr 16 13:48:10 2015 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Thu Apr 16 14:18:32 2015 +0200 @@ -377,7 +377,6 @@ Outer_Syntax.command @{command_keyword nitpick} "try to find a counterexample for a given subgoal using Nitpick" (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))))) diff -r c48d536231fe -r 96a4765ba7d1 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Apr 16 13:48:10 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Apr 16 14:18:32 2015 +0200 @@ -359,7 +359,6 @@ 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) fun string_of_raw_param (key, values) = diff -r c48d536231fe -r 96a4765ba7d1 src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Thu Apr 16 13:48:10 2015 +0200 +++ b/src/HOL/Tools/try0.ML Thu Apr 16 14:18:32 2015 +0200 @@ -154,7 +154,6 @@ fun try0 timeout_opt = fst oo generic_try0 Normal timeout_opt; fun try0_trans quad = - Toplevel.unknown_proof o Toplevel.keep (K () o generic_try0 Normal (SOME default_timeout) quad o Toplevel.proof_of); fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) = (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2); diff -r c48d536231fe -r 96a4765ba7d1 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Thu Apr 16 13:48:10 2015 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Thu Apr 16 14:18:32 2015 +0200 @@ -240,10 +240,7 @@ in ML_Context.eval_source_in opt_ctxt flags source end); val diag_state = Diag_State.get; - -fun diag_goal ctxt = - Proof.goal (Toplevel.proof_of (diag_state ctxt)) - handle Toplevel.UNDEF => error "No goal present"; +val diag_goal = Proof.goal o Toplevel.proof_of o diag_state; val _ = Theory.setup (ML_Antiquotation.value (Binding.qualify true "Isar" @{binding state}) diff -r c48d536231fe -r 96a4765ba7d1 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Thu Apr 16 13:48:10 2015 +0200 +++ b/src/Pure/Isar/proof.ML Thu Apr 16 14:18:32 2015 +0200 @@ -338,7 +338,7 @@ fun find i state = (case try current_goal state of SOME (ctxt, goal) => (ctxt, (i, goal)) - | NONE => find (i + 1) (close_block state handle ERROR _ => error "No goal present")); + | NONE => find (i + 1) (close_block state handle ERROR _ => error "No proof goal")); in val find_goal = find 0 end; fun get_goal state = diff -r c48d536231fe -r 96a4765ba7d1 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Thu Apr 16 13:48:10 2015 +0200 +++ b/src/Pure/Isar/toplevel.ML Thu Apr 16 14:18:32 2015 +0200 @@ -73,7 +73,6 @@ val skip_proof_to_theory: (int -> bool) -> transition -> transition val exec_id: Document_ID.exec -> transition -> transition val unknown_theory: transition -> transition - val unknown_proof: transition -> transition val unknown_context: transition -> transition val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b val add_hook: (transition -> state -> state -> unit) -> unit @@ -164,12 +163,12 @@ val context_of = node_case Context.proof_of Proof.context_of; val generic_theory_of = node_case I (Context.Proof o Proof.context_of); val theory_of = node_case Context.theory_of Proof.theory_of; -val proof_of = node_case (fn _ => raise UNDEF) I; +val proof_of = node_case (fn _ => error "No proof state") I; fun proof_position_of state = (case node_of state of Proof (prf, _) => Proof_Node.position prf - | _ => raise UNDEF); + | _ => ~1); fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.here pos) @@ -357,7 +356,6 @@ empty |> name "" |> position pos |> imperative (fn () => error msg); val unknown_theory = imperative (fn () => warning "Unknown theory context"); -val unknown_proof = imperative (fn () => warning "Unknown proof context"); val unknown_context = imperative (fn () => warning "Unknown context"); diff -r c48d536231fe -r 96a4765ba7d1 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Thu Apr 16 13:48:10 2015 +0200 +++ b/src/Pure/Thy/thy_output.ML Thu Apr 16 14:18:32 2015 +0200 @@ -614,16 +614,12 @@ local -fun proof_state state = - (case try (Proof.goal o Toplevel.proof_of) state of - SOME {goal, ...} => goal - | _ => error "No proof state"); - fun goal_state name main = antiquotation name (Scan.succeed ()) (fn {state, context = ctxt, ...} => fn () => output ctxt [Goal_Display.pretty_goal - (Config.put Goal_Display.show_main_goal main ctxt) (proof_state state)]); + (Config.put Goal_Display.show_main_goal main ctxt) + (#goal (Proof.goal (Toplevel.proof_of state)))]); in diff -r c48d536231fe -r 96a4765ba7d1 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Thu Apr 16 13:48:10 2015 +0200 +++ b/src/Tools/quickcheck.ML Thu Apr 16 14:18:32 2015 +0200 @@ -533,8 +533,8 @@ val _ = Outer_Syntax.command @{command_keyword quickcheck} "try to find counterexample for subgoal" - (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) => - Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i))); + (parse_args -- Scan.optional Parse.nat 1 >> + (fn (args, i) => Toplevel.keep (quickcheck_cmd args i))); (* automatic testing *) diff -r c48d536231fe -r 96a4765ba7d1 src/Tools/solve_direct.ML --- a/src/Tools/solve_direct.ML Thu Apr 16 13:48:10 2015 +0200 +++ b/src/Tools/solve_direct.ML Thu Apr 16 14:18:32 2015 +0200 @@ -94,8 +94,7 @@ val _ = Outer_Syntax.command @{command_keyword solve_direct} "try to solve conjectures directly with existing theorems" - (Scan.succeed (Toplevel.unknown_proof o - Toplevel.keep (ignore o solve_direct o Toplevel.proof_of))); + (Scan.succeed (Toplevel.keep (ignore o solve_direct o Toplevel.proof_of))); (* hook *) diff -r c48d536231fe -r 96a4765ba7d1 src/Tools/try.ML --- a/src/Tools/try.ML Thu Apr 16 13:48:10 2015 +0200 +++ b/src/Tools/try.ML Thu Apr 16 14:18:32 2015 +0200 @@ -77,7 +77,7 @@ val _ = Outer_Syntax.command @{command_keyword try} "try a combination of automatic proving and disproving tools" - (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of))) + (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of))) (* automatic try (TTY) *)