# HG changeset patch
# User wenzelm
# Date 1548851133 -3600
# Node ID 2fc85ce1f557d686964dfbcfc12b7ab28718aaf8
# Parent  8d548b8f63ca3d83a10b9132b1662acf3a459288
discontinued obsolete option "checkpoint";

diff -r 8d548b8f63ca -r 2fc85ce1f557 NEWS
--- a/NEWS	Tue Jan 29 22:47:45 2019 +0100
+++ b/NEWS	Wed Jan 30 13:25:33 2019 +0100
@@ -261,6 +261,8 @@
 
 * Update to Java 11: the latest long-term support version of OpenJDK.
 
+* System option "checkpoint" has been discontinued: obsolete thanks to
+improved memory management in Poly/ML.
 
 
 New in Isabelle2018 (August 2018)
diff -r 8d548b8f63ca -r 2fc85ce1f557 etc/options
--- a/etc/options	Tue Jan 29 22:47:45 2019 +0100
+++ b/etc/options	Wed Jan 30 13:25:33 2019 +0100
@@ -113,9 +113,6 @@
 option process_output_tail : int = 40
   -- "build process output tail shown to user (in lines, 0 = unlimited)"
 
-option checkpoint : bool = false
-  -- "checkpoint for theories during build process (heap compression)"
-
 option profiling : string = ""
   -- "ML profiling (possible values: time, allocations)"
 
diff -r 8d548b8f63ca -r 2fc85ce1f557 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Tue Jan 29 22:47:45 2019 +0100
+++ b/src/Doc/System/Sessions.thy	Wed Jan 30 13:25:33 2019 +0100
@@ -216,13 +216,6 @@
     manual adjustment (on the command-line or within personal settings or
     preferences, not within a session \<^verbatim>\<open>ROOT\<close>).
 
-    \<^item> @{system_option_def "checkpoint"} helps to fine-tune the global heap
-    space management. This is relevant for big sessions that may exhaust the
-    small 32-bit address space of the ML process (which is used by default).
-    When the option is enabled for some \isakeyword{theories} block, a full
-    sharing stage of immutable values in memory happens \<^emph>\<open>before\<close> loading the
-    specified theories.
-
     \<^item> @{system_option_def "condition"} specifies a comma-separated list of
     process environment variables (or Isabelle settings) that are required for
     the subsequent theories to be processed. Conditions are considered
diff -r 8d548b8f63ca -r 2fc85ce1f557 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Tue Jan 29 22:47:45 2019 +0100
+++ b/src/Pure/Tools/build.ML	Wed Jan 30 13:25:33 2019 +0100
@@ -119,8 +119,7 @@
     val conds = filter_out (can getenv_strict) condition;
   in
     if null conds then
-      (if Options.bool options "checkpoint" then ML_Heap.share_common_data () else ();
-        Options.set_default options;
+      (Options.set_default options;
         Isabelle_Process.init_options ();
         Future.fork I;
         (Thy_Info.use_theories context qualifier master_dir