clarified Proofterm.proofs_enabled;
authorwenzelm
Thu Feb 03 19:21:12 2011 +0100 (2011-02-03 ago)
changeset 4169890597e044e5f
parent 41697 19890332febc
child 41699 21492e1c2b5a
clarified Proofterm.proofs_enabled;
src/HOL/Tools/Datatype/datatype_realizer.ML
src/Pure/ProofGeneral/preferences.ML
src/Pure/proofterm.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu Feb 03 18:57:42 2011 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu Feb 03 19:21:12 2011 +0100
     1.3 @@ -214,7 +214,7 @@
     1.4    end;
     1.5  
     1.6  fun add_dt_realizers config names thy =
     1.7 -  if ! Proofterm.proofs < 2 then thy
     1.8 +  if not (Proofterm.proofs_enabled ()) then thy
     1.9    else
    1.10      let
    1.11        val _ = Datatype_Aux.message config "Adding realizers for induction and case analysis ...";
     2.1 --- a/src/Pure/ProofGeneral/preferences.ML	Thu Feb 03 18:57:42 2011 +0100
     2.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Thu Feb 03 19:21:12 2011 +0100
     2.3 @@ -84,7 +84,7 @@
     2.4  
     2.5  val proof_pref = Unsynchronized.setmp Proofterm.proofs 1 (fn () =>
     2.6    let
     2.7 -    fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2);
     2.8 +    fun get () = PgipTypes.bool_to_pgstring (Proofterm.proofs_enabled ());
     2.9      fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1);
    2.10    in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end) ();
    2.11  
     3.1 --- a/src/Pure/proofterm.ML	Thu Feb 03 18:57:42 2011 +0100
     3.2 +++ b/src/Pure/proofterm.ML	Thu Feb 03 19:21:12 2011 +0100
     3.3 @@ -52,6 +52,7 @@
     3.4    val approximate_proof_body: proof -> proof_body
     3.5  
     3.6    (** primitive operations **)
     3.7 +  val proofs_enabled: unit -> bool
     3.8    val proof_combt: proof * term list -> proof
     3.9    val proof_combt': proof * term option list -> proof
    3.10    val proof_combP: proof * proof list -> proof
    3.11 @@ -973,6 +974,7 @@
    3.12  (***** axioms and theorems *****)
    3.13  
    3.14  val proofs = Unsynchronized.ref 2;
    3.15 +fun proofs_enabled () = ! proofs >= 2;
    3.16  
    3.17  fun vars_of t = map Var (rev (Term.add_vars t []));
    3.18  fun frees_of t = map Free (rev (Term.add_frees t []));
    3.19 @@ -1444,7 +1446,7 @@
    3.20  
    3.21      fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
    3.22      val body0 =
    3.23 -      if ! proofs <> 2 then Future.value (make_body0 MinProof)
    3.24 +      if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
    3.25        else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
    3.26        else
    3.27          singleton
    3.28 @@ -1453,6 +1455,7 @@
    3.29  
    3.30      fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
    3.31      val (i, body') =
    3.32 +      (* FIXME non-deterministic!? depends on fulfilled proof*)
    3.33        (case strip_combt (fst (strip_combP prf)) of
    3.34          (PThm (i, ((old_name, prop', NONE), body')), args') =>
    3.35            if (old_name = "" orelse old_name = name) andalso prop1 = prop' andalso args = args'