just one option "skip_proofs", without direct access within the editor (it makes document processing stateful without strong reasons -- monotonic updates already handle goal forks smoothly);
authorwenzelm
Fri Jul 19 17:58:57 2013 +0200 (2013-07-19 ago)
changeset 5271052790e3961fe
parent 52709 0e4bacf21e77
child 52711 155f02cacb2d
just one option "skip_proofs", without direct access within the editor (it makes document processing stateful without strong reasons -- monotonic updates already handle goal forks smoothly);
etc/options
src/Pure/System/isabelle_process.ML
src/Pure/Tools/build.ML
src/Pure/Tools/proof_general_pure.ML
src/Pure/goal.ML
     1.1 --- a/etc/options	Fri Jul 19 17:35:12 2013 +0200
     1.2 +++ b/etc/options	Fri Jul 19 17:58:57 2013 +0200
     1.3 @@ -102,9 +102,6 @@
     1.4  
     1.5  section "Editor Reactivity"
     1.6  
     1.7 -public option editor_skip_proofs : bool = false
     1.8 -  -- "skip over proofs (implicit 'sorry')"
     1.9 -
    1.10  public option editor_load_delay : real = 0.5
    1.11    -- "delay for file load operations (new buffers etc.)"
    1.12  
     2.1 --- a/src/Pure/System/isabelle_process.ML	Fri Jul 19 17:35:12 2013 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.ML	Fri Jul 19 17:58:57 2013 +0200
     2.3 @@ -229,7 +229,6 @@
     2.4          Future.ML_statistics := true;
     2.5          Multithreading.trace := Options.int options "threads_trace";
     2.6          Multithreading.max_threads := Options.int options "threads";
     2.7 -        Goal.skip_proofs := Options.bool options "editor_skip_proofs";
     2.8          Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0)
     2.9        end);
    2.10  
     3.1 --- a/src/Pure/Tools/build.ML	Fri Jul 19 17:35:12 2013 +0200
     3.2 +++ b/src/Pure/Tools/build.ML	Fri Jul 19 17:58:57 2013 +0200
     3.3 @@ -109,7 +109,6 @@
     3.4      |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
     3.5      |> Unsynchronized.setmp Future.ML_statistics true
     3.6      |> no_document options ? Present.no_document
     3.7 -    |> Unsynchronized.setmp Goal.skip_proofs (Options.bool options "skip_proofs")
     3.8      |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
     3.9      |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
    3.10  
     4.1 --- a/src/Pure/Tools/proof_general_pure.ML	Fri Jul 19 17:35:12 2013 +0200
     4.2 +++ b/src/Pure/Tools/proof_general_pure.ML	Fri Jul 19 17:58:57 2013 +0200
     4.3 @@ -143,9 +143,9 @@
     4.4      "Take a few short cuts";
     4.5  
     4.6  val _ =
     4.7 -  ProofGeneral.preference_bool ProofGeneral.category_proof
     4.8 +  ProofGeneral.preference_option ProofGeneral.category_proof
     4.9      NONE
    4.10 -    Goal.skip_proofs
    4.11 +    @{option skip_proofs}
    4.12      "skip-proofs"
    4.13      "Skip over proofs";
    4.14  
     5.1 --- a/src/Pure/goal.ML	Fri Jul 19 17:35:12 2013 +0200
     5.2 +++ b/src/Pure/goal.ML	Fri Jul 19 17:58:57 2013 +0200
     5.3 @@ -6,7 +6,6 @@
     5.4  
     5.5  signature BASIC_GOAL =
     5.6  sig
     5.7 -  val skip_proofs: bool Unsynchronized.ref
     5.8    val parallel_proofs: int Unsynchronized.ref
     5.9    val SELECT_GOAL: tactic -> int -> tactic
    5.10    val PREFER_GOAL: tactic -> int -> tactic
    5.11 @@ -200,10 +199,8 @@
    5.12  
    5.13  (* scheduling parameters *)
    5.14  
    5.15 -val skip_proofs = Unsynchronized.ref false;
    5.16 -
    5.17  fun skip_proofs_enabled () =
    5.18 -  let val skip = ! skip_proofs in
    5.19 +  let val skip = Options.default_bool "skip_proofs" in
    5.20      if Proofterm.proofs_enabled () andalso skip then
    5.21        (warning "Proof terms enabled -- cannot skip proofs"; false)
    5.22      else skip