# HG changeset patch
# User wenzelm
# Date 1372769281 -7200
# Node ID 812215680f6d13d1151c99d0df9f6091f10c6b0f
# Parent  d802431fe3569404c86ce9ba48984a3e4706296b
clarified Proofterm.proofs vs. Goal.skip_proofs;

diff -r d802431fe356 -r 812215680f6d src/Doc/ROOT
--- a/src/Doc/ROOT	Mon Jul 01 15:08:29 2013 +0200
+++ b/src/Doc/ROOT	Tue Jul 02 14:48:01 2013 +0200
@@ -81,7 +81,7 @@
     Proof
     Syntax
     Tactic
-  theories [skip_proofs = false, parallel_proofs = 0]
+  theories [parallel_proofs = 0]
     Logic
   files
     "../prepare_document"
diff -r d802431fe356 -r 812215680f6d src/HOL/ROOT
--- a/src/HOL/ROOT	Mon Jul 01 15:08:29 2013 +0200
+++ b/src/HOL/ROOT	Tue Jul 02 14:48:01 2013 +0200
@@ -16,7 +16,7 @@
   description {*
     HOL-Main with explicit proof terms.
   *}
-  options [document = false, skip_proofs = false]
+  options [document = false]
   theories Proofs (*sequential change of global flag!*)
   theories Main
   files
@@ -357,7 +357,7 @@
   theories Decision_Procs
 
 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
-  options [document = false, skip_proofs = false, parallel_proofs = 0]
+  options [document = false, parallel_proofs = 0]
   theories
     Hilbert_Classical
     XML_Data
@@ -366,7 +366,7 @@
   description {*
     Examples for program extraction in Higher-Order Logic.
   *}
-  options [condition = ISABELLE_POLYML, skip_proofs = false, parallel_proofs = 0]
+  options [condition = ISABELLE_POLYML, parallel_proofs = 0]
   theories [document = false]
     "~~/src/HOL/Library/Code_Target_Numeral"
     "~~/src/HOL/Library/Monad_Syntax"
@@ -391,7 +391,7 @@
     The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
     theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
   *}
-  options [document_graph, print_mode = "no_brackets", skip_proofs = false, parallel_proofs = 0]
+  options [document_graph, print_mode = "no_brackets", parallel_proofs = 0]
   theories [document = false]
     "~~/src/HOL/Library/Code_Target_Int"
   theories
diff -r d802431fe356 -r 812215680f6d src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Jul 01 15:08:29 2013 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jul 02 14:48:01 2013 +0200
@@ -517,7 +517,7 @@
   (fn Theory (gthy, _) =>
     let
       val (finish, prf) = init int gthy;
-      val skip = ! Goal.skip_proofs;
+      val skip = Goal.skip_proofs_enabled ();
       val (is_goal, no_skip) =
         (true, Proof.schematic_goal prf) handle ERROR _ => (false, true);
       val _ =
diff -r d802431fe356 -r 812215680f6d src/Pure/goal.ML
--- a/src/Pure/goal.ML	Mon Jul 01 15:08:29 2013 +0200
+++ b/src/Pure/goal.ML	Tue Jul 02 14:48:01 2013 +0200
@@ -30,6 +30,7 @@
   val peek_futures: serial -> unit future list
   val reset_futures: unit -> Future.group list
   val shutdown_futures: unit -> unit
+  val skip_proofs_enabled: unit -> bool
   val future_enabled_level: int -> bool
   val future_enabled: unit -> bool
   val future_enabled_nested: int -> bool
@@ -197,6 +198,13 @@
 
 val skip_proofs = Unsynchronized.ref false;
 
+fun skip_proofs_enabled () =
+  let val skip = ! skip_proofs in
+    if Proofterm.proofs_enabled () andalso skip then
+      (warning "Proof terms enabled -- cannot skip proofs"; false)
+    else skip
+  end;
+
 val parallel_proofs = Unsynchronized.ref 1;
 
 fun future_enabled_level n =
@@ -277,7 +285,7 @@
 
     val schematic = exists is_schematic props;
     val future = future_enabled ();
-    val skip = not immediate andalso not schematic andalso future andalso ! skip_proofs;
+    val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled ();
 
     val pos = Position.thread_data ();
     fun err msg = cat_error msg