clarified Proofterm.proofs vs. Goal.skip_proofs;
authorwenzelm
Tue Jul 02 14:48:01 2013 +0200 (2013-07-02)
changeset 52499812215680f6d
parent 52498 d802431fe356
child 52500 9b44e7df9350
clarified Proofterm.proofs vs. Goal.skip_proofs;
src/Doc/ROOT
src/HOL/ROOT
src/Pure/Isar/toplevel.ML
src/Pure/goal.ML
     1.1 --- a/src/Doc/ROOT	Mon Jul 01 15:08:29 2013 +0200
     1.2 +++ b/src/Doc/ROOT	Tue Jul 02 14:48:01 2013 +0200
     1.3 @@ -81,7 +81,7 @@
     1.4      Proof
     1.5      Syntax
     1.6      Tactic
     1.7 -  theories [skip_proofs = false, parallel_proofs = 0]
     1.8 +  theories [parallel_proofs = 0]
     1.9      Logic
    1.10    files
    1.11      "../prepare_document"
     2.1 --- a/src/HOL/ROOT	Mon Jul 01 15:08:29 2013 +0200
     2.2 +++ b/src/HOL/ROOT	Tue Jul 02 14:48:01 2013 +0200
     2.3 @@ -16,7 +16,7 @@
     2.4    description {*
     2.5      HOL-Main with explicit proof terms.
     2.6    *}
     2.7 -  options [document = false, skip_proofs = false]
     2.8 +  options [document = false]
     2.9    theories Proofs (*sequential change of global flag!*)
    2.10    theories Main
    2.11    files
    2.12 @@ -357,7 +357,7 @@
    2.13    theories Decision_Procs
    2.14  
    2.15  session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
    2.16 -  options [document = false, skip_proofs = false, parallel_proofs = 0]
    2.17 +  options [document = false, parallel_proofs = 0]
    2.18    theories
    2.19      Hilbert_Classical
    2.20      XML_Data
    2.21 @@ -366,7 +366,7 @@
    2.22    description {*
    2.23      Examples for program extraction in Higher-Order Logic.
    2.24    *}
    2.25 -  options [condition = ISABELLE_POLYML, skip_proofs = false, parallel_proofs = 0]
    2.26 +  options [condition = ISABELLE_POLYML, parallel_proofs = 0]
    2.27    theories [document = false]
    2.28      "~~/src/HOL/Library/Code_Target_Numeral"
    2.29      "~~/src/HOL/Library/Monad_Syntax"
    2.30 @@ -391,7 +391,7 @@
    2.31      The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
    2.32      theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
    2.33    *}
    2.34 -  options [document_graph, print_mode = "no_brackets", skip_proofs = false, parallel_proofs = 0]
    2.35 +  options [document_graph, print_mode = "no_brackets", parallel_proofs = 0]
    2.36    theories [document = false]
    2.37      "~~/src/HOL/Library/Code_Target_Int"
    2.38    theories
     3.1 --- a/src/Pure/Isar/toplevel.ML	Mon Jul 01 15:08:29 2013 +0200
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Jul 02 14:48:01 2013 +0200
     3.3 @@ -517,7 +517,7 @@
     3.4    (fn Theory (gthy, _) =>
     3.5      let
     3.6        val (finish, prf) = init int gthy;
     3.7 -      val skip = ! Goal.skip_proofs;
     3.8 +      val skip = Goal.skip_proofs_enabled ();
     3.9        val (is_goal, no_skip) =
    3.10          (true, Proof.schematic_goal prf) handle ERROR _ => (false, true);
    3.11        val _ =
     4.1 --- a/src/Pure/goal.ML	Mon Jul 01 15:08:29 2013 +0200
     4.2 +++ b/src/Pure/goal.ML	Tue Jul 02 14:48:01 2013 +0200
     4.3 @@ -30,6 +30,7 @@
     4.4    val peek_futures: serial -> unit future list
     4.5    val reset_futures: unit -> Future.group list
     4.6    val shutdown_futures: unit -> unit
     4.7 +  val skip_proofs_enabled: unit -> bool
     4.8    val future_enabled_level: int -> bool
     4.9    val future_enabled: unit -> bool
    4.10    val future_enabled_nested: int -> bool
    4.11 @@ -197,6 +198,13 @@
    4.12  
    4.13  val skip_proofs = Unsynchronized.ref false;
    4.14  
    4.15 +fun skip_proofs_enabled () =
    4.16 +  let val skip = ! skip_proofs in
    4.17 +    if Proofterm.proofs_enabled () andalso skip then
    4.18 +      (warning "Proof terms enabled -- cannot skip proofs"; false)
    4.19 +    else skip
    4.20 +  end;
    4.21 +
    4.22  val parallel_proofs = Unsynchronized.ref 1;
    4.23  
    4.24  fun future_enabled_level n =
    4.25 @@ -277,7 +285,7 @@
    4.26  
    4.27      val schematic = exists is_schematic props;
    4.28      val future = future_enabled ();
    4.29 -    val skip = not immediate andalso not schematic andalso future andalso ! skip_proofs;
    4.30 +    val skip = not immediate andalso not schematic andalso future andalso skip_proofs_enabled ();
    4.31  
    4.32      val pos = Position.thread_data ();
    4.33      fun err msg = cat_error msg