# HG changeset patch
# User wenzelm
# Date 1350476454 -7200
# Node ID 89eff795f75782b08d378b430fe99d7f521c6616
# Parent  00ea087e83d8215370307e2241839924db4447f9
skipped proofs appear as "bad" without counting as error;

diff -r 00ea087e83d8 -r 89eff795f757 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Oct 17 13:20:08 2012 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Oct 17 14:20:54 2012 +0200
@@ -1002,22 +1002,33 @@
 
 (* concluding steps *)
 
+local
+
 fun terminal_proof qeds initial terminal =
   proof_results (SOME initial) #> Seq.maps_results (qeds (#2 (#2 initial), terminal))
   #> Seq.the_result "";
 
+fun skipped_proof x =
+  (Output.report (Markup.markup Isabelle_Markup.bad "Skipped proof"); x);
+
+in
+
 fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true);
 val local_default_proof = local_terminal_proof ((Method.default_text, Position.no_range), NONE);
 val local_immediate_proof = local_terminal_proof ((Method.this_text, Position.no_range), NONE);
-fun local_skip_proof int = local_terminal_proof ((Method.sorry_text int, Position.no_range), NONE);
+fun local_skip_proof int =
+  local_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) #> skipped_proof;
 val local_done_proof = terminal_proof local_qeds (Method.done_text, Position.no_range) (NONE, false);
 
 fun global_terminal_proof (text, opt_text) = terminal_proof global_qeds text (opt_text, true);
 val global_default_proof = global_terminal_proof ((Method.default_text, Position.no_range), NONE);
 val global_immediate_proof = global_terminal_proof ((Method.this_text, Position.no_range), NONE);
-fun global_skip_proof int = global_terminal_proof ((Method.sorry_text int, Position.no_range), NONE);
+fun global_skip_proof int =
+  global_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) #> skipped_proof;
 val global_done_proof = terminal_proof global_qeds (Method.done_text, Position.no_range) (NONE, false);
 
+end;
+
 
 (* common goal statements *)