explicit error for Toplevel.proof_of;
authorwenzelm
Thu Apr 16 14:18:32 2015 +0200 (2015-04-16)
changeset 6009496a4765ba7d1
parent 60093 c48d536231fe
child 60095 35f626b11422
explicit error for Toplevel.proof_of;
eliminated obsolete Toplevel.unknown_proof;
more total Toplevel.proof_position_of;
NEWS
src/Doc/Implementation/Integration.thy
src/HOL/Library/refute.ML
src/HOL/Tools/Nitpick/nitpick_commands.ML
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
src/HOL/Tools/try0.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/toplevel.ML
src/Pure/Thy/thy_output.ML
src/Tools/quickcheck.ML
src/Tools/solve_direct.ML
src/Tools/try.ML
     1.1 --- a/NEWS	Thu Apr 16 13:48:10 2015 +0200
     1.2 +++ b/NEWS	Thu Apr 16 14:18:32 2015 +0200
     1.3 @@ -398,6 +398,9 @@
     1.4  derivatives) instead, which is not affected by the change. Potential
     1.5  INCOMPATIBILITY in rare applications of Name_Space.intern.
     1.6  
     1.7 +* Subtle change of error semantics of Toplevel.proof_of: regular user
     1.8 +ERROR instead of internal Toplevel.UNDEF.
     1.9 +
    1.10  * Basic combinators map, fold, fold_map, split_list, apply are available
    1.11  as parameterized antiquotations, e.g. @{map 4} for lists of quadruples.
    1.12  
     2.1 --- a/src/Doc/Implementation/Integration.thy	Thu Apr 16 13:48:10 2015 +0200
     2.2 +++ b/src/Doc/Implementation/Integration.thy	Thu Apr 16 14:18:32 2015 +0200
     2.3 @@ -62,7 +62,7 @@
     2.4    for an empty toplevel state.
     2.5  
     2.6    \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
     2.7 -  state if available, otherwise it raises @{ML Toplevel.UNDEF}.
     2.8 +  state if available, otherwise it raises an error.
     2.9  
    2.10    \end{description}
    2.11  \<close>
     3.1 --- a/src/HOL/Library/refute.ML	Thu Apr 16 13:48:10 2015 +0200
     3.2 +++ b/src/HOL/Library/refute.ML	Thu Apr 16 14:18:32 2015 +0200
     3.3 @@ -2969,7 +2969,6 @@
     3.4      "try to find a model that refutes a given subgoal"
     3.5      (scan_parms -- Scan.optional Parse.nat 1 >>
     3.6        (fn (parms, i) =>
     3.7 -        Toplevel.unknown_proof o
     3.8          Toplevel.keep (fn state =>
     3.9            let
    3.10              val ctxt = Toplevel.context_of state;
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Thu Apr 16 13:48:10 2015 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Thu Apr 16 14:18:32 2015 +0200
     4.3 @@ -377,7 +377,6 @@
     4.4    Outer_Syntax.command @{command_keyword nitpick}
     4.5      "try to find a counterexample for a given subgoal using Nitpick"
     4.6      (parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) =>
     4.7 -      Toplevel.unknown_proof o
     4.8        Toplevel.keep (fn state =>
     4.9          ignore (pick_nits params Normal i (Toplevel.proof_position_of state)
    4.10            (Toplevel.proof_of state)))))
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Apr 16 13:48:10 2015 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Apr 16 14:18:32 2015 +0200
     5.3 @@ -359,7 +359,6 @@
     5.4    end
     5.5  
     5.6  fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) =
     5.7 -  Toplevel.unknown_proof o
     5.8    Toplevel.keep (hammer_away params subcommand opt_i fact_override o Toplevel.proof_of)
     5.9  
    5.10  fun string_of_raw_param (key, values) =
     6.1 --- a/src/HOL/Tools/try0.ML	Thu Apr 16 13:48:10 2015 +0200
     6.2 +++ b/src/HOL/Tools/try0.ML	Thu Apr 16 14:18:32 2015 +0200
     6.3 @@ -154,7 +154,6 @@
     6.4  fun try0 timeout_opt = fst oo generic_try0 Normal timeout_opt;
     6.5  
     6.6  fun try0_trans quad =
     6.7 -  Toplevel.unknown_proof o
     6.8    Toplevel.keep (K () o generic_try0 Normal (SOME default_timeout) quad o Toplevel.proof_of);
     6.9  
    6.10  fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) = (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2);
     7.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Apr 16 13:48:10 2015 +0200
     7.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Apr 16 14:18:32 2015 +0200
     7.3 @@ -240,10 +240,7 @@
     7.4    in ML_Context.eval_source_in opt_ctxt flags source end);
     7.5  
     7.6  val diag_state = Diag_State.get;
     7.7 -
     7.8 -fun diag_goal ctxt =
     7.9 -  Proof.goal (Toplevel.proof_of (diag_state ctxt))
    7.10 -    handle Toplevel.UNDEF => error "No goal present";
    7.11 +val diag_goal = Proof.goal o Toplevel.proof_of o diag_state;
    7.12  
    7.13  val _ = Theory.setup
    7.14    (ML_Antiquotation.value (Binding.qualify true "Isar" @{binding state})
     8.1 --- a/src/Pure/Isar/proof.ML	Thu Apr 16 13:48:10 2015 +0200
     8.2 +++ b/src/Pure/Isar/proof.ML	Thu Apr 16 14:18:32 2015 +0200
     8.3 @@ -338,7 +338,7 @@
     8.4    fun find i state =
     8.5      (case try current_goal state of
     8.6        SOME (ctxt, goal) => (ctxt, (i, goal))
     8.7 -    | NONE => find (i + 1) (close_block state handle ERROR _ => error "No goal present"));
     8.8 +    | NONE => find (i + 1) (close_block state handle ERROR _ => error "No proof goal"));
     8.9  in val find_goal = find 0 end;
    8.10  
    8.11  fun get_goal state =
     9.1 --- a/src/Pure/Isar/toplevel.ML	Thu Apr 16 13:48:10 2015 +0200
     9.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Apr 16 14:18:32 2015 +0200
     9.3 @@ -73,7 +73,6 @@
     9.4    val skip_proof_to_theory: (int -> bool) -> transition -> transition
     9.5    val exec_id: Document_ID.exec -> transition -> transition
     9.6    val unknown_theory: transition -> transition
     9.7 -  val unknown_proof: transition -> transition
     9.8    val unknown_context: transition -> transition
     9.9    val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
    9.10    val add_hook: (transition -> state -> state -> unit) -> unit
    9.11 @@ -164,12 +163,12 @@
    9.12  val context_of = node_case Context.proof_of Proof.context_of;
    9.13  val generic_theory_of = node_case I (Context.Proof o Proof.context_of);
    9.14  val theory_of = node_case Context.theory_of Proof.theory_of;
    9.15 -val proof_of = node_case (fn _ => raise UNDEF) I;
    9.16 +val proof_of = node_case (fn _ => error "No proof state") I;
    9.17  
    9.18  fun proof_position_of state =
    9.19    (case node_of state of
    9.20      Proof (prf, _) => Proof_Node.position prf
    9.21 -  | _ => raise UNDEF);
    9.22 +  | _ => ~1);
    9.23  
    9.24  fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
    9.25    | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.here pos)
    9.26 @@ -357,7 +356,6 @@
    9.27    empty |> name "<malformed>" |> position pos |> imperative (fn () => error msg);
    9.28  
    9.29  val unknown_theory = imperative (fn () => warning "Unknown theory context");
    9.30 -val unknown_proof = imperative (fn () => warning "Unknown proof context");
    9.31  val unknown_context = imperative (fn () => warning "Unknown context");
    9.32  
    9.33  
    10.1 --- a/src/Pure/Thy/thy_output.ML	Thu Apr 16 13:48:10 2015 +0200
    10.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Apr 16 14:18:32 2015 +0200
    10.3 @@ -614,16 +614,12 @@
    10.4  
    10.5  local
    10.6  
    10.7 -fun proof_state state =
    10.8 -  (case try (Proof.goal o Toplevel.proof_of) state of
    10.9 -    SOME {goal, ...} => goal
   10.10 -  | _ => error "No proof state");
   10.11 -
   10.12  fun goal_state name main = antiquotation name (Scan.succeed ())
   10.13    (fn {state, context = ctxt, ...} => fn () =>
   10.14      output ctxt
   10.15        [Goal_Display.pretty_goal
   10.16 -        (Config.put Goal_Display.show_main_goal main ctxt) (proof_state state)]);
   10.17 +        (Config.put Goal_Display.show_main_goal main ctxt)
   10.18 +        (#goal (Proof.goal (Toplevel.proof_of state)))]);
   10.19  
   10.20  in
   10.21  
    11.1 --- a/src/Tools/quickcheck.ML	Thu Apr 16 13:48:10 2015 +0200
    11.2 +++ b/src/Tools/quickcheck.ML	Thu Apr 16 14:18:32 2015 +0200
    11.3 @@ -533,8 +533,8 @@
    11.4  val _ =
    11.5    Outer_Syntax.command @{command_keyword quickcheck}
    11.6      "try to find counterexample for subgoal"
    11.7 -    (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) =>
    11.8 -      Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i)));
    11.9 +    (parse_args -- Scan.optional Parse.nat 1 >>
   11.10 +      (fn (args, i) => Toplevel.keep (quickcheck_cmd args i)));
   11.11  
   11.12  
   11.13  (* automatic testing *)
    12.1 --- a/src/Tools/solve_direct.ML	Thu Apr 16 13:48:10 2015 +0200
    12.2 +++ b/src/Tools/solve_direct.ML	Thu Apr 16 14:18:32 2015 +0200
    12.3 @@ -94,8 +94,7 @@
    12.4  val _ =
    12.5    Outer_Syntax.command @{command_keyword solve_direct}
    12.6      "try to solve conjectures directly with existing theorems"
    12.7 -    (Scan.succeed (Toplevel.unknown_proof o
    12.8 -      Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
    12.9 +    (Scan.succeed (Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
   12.10  
   12.11  
   12.12  (* hook *)
    13.1 --- a/src/Tools/try.ML	Thu Apr 16 13:48:10 2015 +0200
    13.2 +++ b/src/Tools/try.ML	Thu Apr 16 14:18:32 2015 +0200
    13.3 @@ -77,7 +77,7 @@
    13.4  val _ =
    13.5    Outer_Syntax.command @{command_keyword try}
    13.6      "try a combination of automatic proving and disproving tools"
    13.7 -    (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
    13.8 +    (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
    13.9  
   13.10  
   13.11  (* automatic try (TTY) *)