# HG changeset patch
# User wenzelm
# Date 1429726483 -7200
# Node ID 906de96ba68a889b4a74271afb07e986f6bee724
# Parent  0d3a621270579e2c76b2f7e508e84a6e7b7aaee2
allow diagnostic proof commands with skip_proofs;

diff -r 0d3a62127057 -r 906de96ba68a src/HOL/Library/refute.ML
--- a/src/HOL/Library/refute.ML	Wed Apr 22 19:48:32 2015 +0200
+++ b/src/HOL/Library/refute.ML	Wed Apr 22 20:14:43 2015 +0200
@@ -2969,7 +2969,7 @@
     "try to find a model that refutes a given subgoal"
     (scan_parms -- Scan.optional Parse.nat 1 >>
       (fn (parms, i) =>
-        Toplevel.keep (fn state =>
+        Toplevel.keep_proof (fn state =>
           let
             val ctxt = Toplevel.context_of state;
             val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state);
diff -r 0d3a62127057 -r 906de96ba68a src/HOL/Tools/Nitpick/nitpick_commands.ML
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Wed Apr 22 19:48:32 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Wed Apr 22 20:14:43 2015 +0200
@@ -377,7 +377,7 @@
   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.keep (fn state =>
+      Toplevel.keep_proof (fn state =>
         ignore (pick_nits params Normal i (Toplevel.proof_position_of state)
           (Toplevel.proof_of state)))))
 
diff -r 0d3a62127057 -r 906de96ba68a src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Apr 22 19:48:32 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Apr 22 20:14:43 2015 +0200
@@ -359,7 +359,7 @@
   end
 
 fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) =
-  Toplevel.keep (hammer_away params subcommand opt_i fact_override o Toplevel.proof_of)
+  Toplevel.keep_proof (hammer_away params subcommand opt_i fact_override o Toplevel.proof_of)
 
 fun string_of_raw_param (key, values) =
   key ^ (case implode_param values of "" => "" | value => " = " ^ value)
diff -r 0d3a62127057 -r 906de96ba68a src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Wed Apr 22 19:48:32 2015 +0200
+++ b/src/HOL/Tools/try0.ML	Wed Apr 22 20:14:43 2015 +0200
@@ -154,7 +154,8 @@
 fun try0 timeout_opt = fst oo generic_try0 Normal timeout_opt;
 
 fun try0_trans quad =
-  Toplevel.keep (K () o generic_try0 Normal (SOME default_timeout) quad o Toplevel.proof_of);
+  Toplevel.keep_proof
+    (ignore 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 0d3a62127057 -r 906de96ba68a src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Apr 22 19:48:32 2015 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Apr 22 20:14:43 2015 +0200
@@ -40,6 +40,7 @@
   val exit: transition -> transition
   val keep: (state -> unit) -> transition -> transition
   val keep': (bool -> state -> unit) -> transition -> transition
+  val keep_proof: (state -> unit) -> transition -> transition
   val ignored: Position.T -> transition
   val is_ignored: transition -> bool
   val malformed: Position.T -> string -> transition
@@ -345,6 +346,12 @@
 
 fun keep f = add_trans (Keep (fn _ => f));
 
+fun keep_proof f =
+  keep (fn st =>
+    if is_proof st then f st
+    else if is_skipped_proof st then ()
+    else warning "No proof state");
+
 fun ignored pos = empty |> name "<ignored>" |> position pos |> keep (fn _ => ());
 fun is_ignored tr = name_of tr = "<ignored>";
 
diff -r 0d3a62127057 -r 906de96ba68a src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Wed Apr 22 19:48:32 2015 +0200
+++ b/src/Tools/quickcheck.ML	Wed Apr 22 20:14:43 2015 +0200
@@ -510,8 +510,8 @@
 fun quickcheck args i state =
   Option.map (the o get_first counterexample_of) (fst (gen_quickcheck args i state));
 
-fun quickcheck_cmd args i state =
-  gen_quickcheck args i (Toplevel.proof_of state)
+fun quickcheck_cmd args i st =
+  gen_quickcheck args i (Toplevel.proof_of st)
   |> apfst (Option.map (the o get_first response_of))
   |> (fn (r, state) =>
       writeln (Pretty.string_of
@@ -534,7 +534,7 @@
   Outer_Syntax.command @{command_keyword quickcheck}
     "try to find counterexample for subgoal"
     (parse_args -- Scan.optional Parse.nat 1 >>
-      (fn (args, i) => Toplevel.keep (quickcheck_cmd args i)));
+      (fn (args, i) => Toplevel.keep_proof (quickcheck_cmd args i)));
 
 
 (* automatic testing *)
diff -r 0d3a62127057 -r 906de96ba68a src/Tools/solve_direct.ML
--- a/src/Tools/solve_direct.ML	Wed Apr 22 19:48:32 2015 +0200
+++ b/src/Tools/solve_direct.ML	Wed Apr 22 20:14:43 2015 +0200
@@ -94,7 +94,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword 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.keep_proof (ignore o solve_direct o Toplevel.proof_of)));
 
 
 (* hook *)
diff -r 0d3a62127057 -r 906de96ba68a src/Tools/try.ML
--- a/src/Tools/try.ML	Wed Apr 22 19:48:32 2015 +0200
+++ b/src/Tools/try.ML	Wed Apr 22 20:14:43 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.keep (ignore o try_tools o Toplevel.proof_of)))
+    (Scan.succeed (Toplevel.keep_proof (ignore o try_tools o Toplevel.proof_of)))
 
 
 (* automatic try (TTY) *)