# HG changeset patch
# User wenzelm
# Date 1491761820 -7200
# Node ID 9bc3b57c1fa7979a404139e8ea7006233a3ac6ca
# Parent  fae6051ec19242de361a7625fc9fb815c2d26a30
added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;

diff -r fae6051ec192 -r 9bc3b57c1fa7 NEWS
--- a/NEWS	Sun Apr 09 19:56:52 2017 +0200
+++ b/NEWS	Sun Apr 09 20:17:00 2017 +0200
@@ -166,6 +166,14 @@
 ISABELLE_PLATFORM64.
 
 
+*** System ***
+
+* System option "record_proofs" allows to change the global
+Proofterm.proofs variable for a session. Regular values are are 0, 1, 2;
+a negative value means the current state in the ML heap image remains
+unchanged.
+
+
 
 New in Isabelle2016-1 (December 2016)
 -------------------------------------
diff -r fae6051ec192 -r 9bc3b57c1fa7 etc/options
--- a/etc/options	Sun Apr 09 19:56:52 2017 +0200
+++ b/etc/options	Sun Apr 09 20:17:00 2017 +0200
@@ -82,6 +82,8 @@
 
 section "Detail of Proof Checking"
 
+option record_proofs : int = -1
+  -- "set level of proofterm recording: 0, 1, 2, negative means unchanged"
 option quick_and_dirty : bool = false
   -- "if true then some tools will OMIT some proofs"
 option skip_proofs : bool = false
diff -r fae6051ec192 -r 9bc3b57c1fa7 src/HOL/Proofs.thy
--- a/src/HOL/Proofs.thy	Sun Apr 09 19:56:52 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-theory Proofs
-imports Pure
-begin
-
-ML "Proofterm.proofs := 2"
-
-end
-
diff -r fae6051ec192 -r 9bc3b57c1fa7 src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Apr 09 19:56:52 2017 +0200
+++ b/src/HOL/ROOT	Sun Apr 09 20:17:00 2017 +0200
@@ -18,8 +18,7 @@
   description {*
     HOL-Main with explicit proof terms.
   *}
-  options [document = false, quick_and_dirty = false, parallel_proofs = 0]
-  theories Proofs (*sequential change of global flag!*)
+  options [document = false, quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
   theories "~~/src/HOL/Library/Old_Datatype"
   files
     "Tools/Quickcheck/Narrowing_Engine.hs"
diff -r fae6051ec192 -r 9bc3b57c1fa7 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Sun Apr 09 19:56:52 2017 +0200
+++ b/src/Pure/System/isabelle_process.ML	Sun Apr 09 20:17:00 2017 +0200
@@ -219,6 +219,8 @@
   Multithreading.trace := Options.default_int "threads_trace";
   Multithreading.max_threads_update (Options.default_int "threads");
   Goal.parallel_proofs := Options.default_int "parallel_proofs";
+  let val proofs = Options.default_int "record_proofs"
+  in if proofs < 0 then () else Proofterm.proofs := proofs end;
   Printer.show_markup_default := false);
 
 fun init_options_interactive () =