# HG changeset patch
# User wenzelm
# Date 1374249537 -7200
# Node ID 52790e3961fe016fa56caa1baea6081c08fe7b37
# Parent  0e4bacf21e771db3480ab8bd36f6d2cd5ca351ad
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);

diff -r 0e4bacf21e77 -r 52790e3961fe etc/options
--- a/etc/options	Fri Jul 19 17:35:12 2013 +0200
+++ b/etc/options	Fri Jul 19 17:58:57 2013 +0200
@@ -102,9 +102,6 @@
 
 section "Editor Reactivity"
 
-public option editor_skip_proofs : bool = false
-  -- "skip over proofs (implicit 'sorry')"
-
 public option editor_load_delay : real = 0.5
   -- "delay for file load operations (new buffers etc.)"
 
diff -r 0e4bacf21e77 -r 52790e3961fe src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Fri Jul 19 17:35:12 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML	Fri Jul 19 17:58:57 2013 +0200
@@ -229,7 +229,6 @@
         Future.ML_statistics := true;
         Multithreading.trace := Options.int options "threads_trace";
         Multithreading.max_threads := Options.int options "threads";
-        Goal.skip_proofs := Options.bool options "editor_skip_proofs";
         Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0)
       end);
 
diff -r 0e4bacf21e77 -r 52790e3961fe src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Fri Jul 19 17:35:12 2013 +0200
+++ b/src/Pure/Tools/build.ML	Fri Jul 19 17:58:57 2013 +0200
@@ -109,7 +109,6 @@
     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
     |> Unsynchronized.setmp Future.ML_statistics true
     |> no_document options ? Present.no_document
-    |> Unsynchronized.setmp Goal.skip_proofs (Options.bool options "skip_proofs")
     |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
     |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
 
diff -r 0e4bacf21e77 -r 52790e3961fe src/Pure/Tools/proof_general_pure.ML
--- a/src/Pure/Tools/proof_general_pure.ML	Fri Jul 19 17:35:12 2013 +0200
+++ b/src/Pure/Tools/proof_general_pure.ML	Fri Jul 19 17:58:57 2013 +0200
@@ -143,9 +143,9 @@
     "Take a few short cuts";
 
 val _ =
-  ProofGeneral.preference_bool ProofGeneral.category_proof
+  ProofGeneral.preference_option ProofGeneral.category_proof
     NONE
-    Goal.skip_proofs
+    @{option skip_proofs}
     "skip-proofs"
     "Skip over proofs";
 
diff -r 0e4bacf21e77 -r 52790e3961fe src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri Jul 19 17:35:12 2013 +0200
+++ b/src/Pure/goal.ML	Fri Jul 19 17:58:57 2013 +0200
@@ -6,7 +6,6 @@
 
 signature BASIC_GOAL =
 sig
-  val skip_proofs: bool Unsynchronized.ref
   val parallel_proofs: int Unsynchronized.ref
   val SELECT_GOAL: tactic -> int -> tactic
   val PREFER_GOAL: tactic -> int -> tactic
@@ -200,10 +199,8 @@
 
 (* scheduling parameters *)
 
-val skip_proofs = Unsynchronized.ref false;
-
 fun skip_proofs_enabled () =
-  let val skip = ! skip_proofs in
+  let val skip = Options.default_bool "skip_proofs" in
     if Proofterm.proofs_enabled () andalso skip then
       (warning "Proof terms enabled -- cannot skip proofs"; false)
     else skip