# HG changeset patch
# User wenzelm
# Date 1569842629 -7200
# Node ID 2071dbe5547dab5845a45b5f964e830c6bf08cc6
# Parent  8abda6f6b7002b316e73d4fefc9efa6cede2a0bc
added dump_options: disabled by default;

diff -r 8abda6f6b700 -r 2071dbe5547d src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Mon Sep 30 13:11:22 2019 +0200
+++ b/src/Doc/System/Sessions.thy	Mon Sep 30 13:23:49 2019 +0200
@@ -546,6 +546,7 @@
   Options are:
     -A NAMES     dump named aspects (default: ...)
     -B NAME      include session NAME and all descendants
+    -C           observe option dump_checkpoint for theories
     -D DIR       include session directory and select its sessions
     -O DIR       output directory for dumped files (default: "dump")
     -R           operate on requirements of selected sessions
@@ -582,6 +583,11 @@
   \<^verbatim>\<open>isabelle.Dump.dump()\<close> takes aspects as user-defined operations on the
   final PIDE state and document version. This allows to imitate Prover IDE
   rendering under program control.
+
+  \<^medskip> Option \<^verbatim>\<open>-C\<close> observes option \<^verbatim>\<open>dump_checkpoint\<close> within the
+  \isakeyword{theories} specification of session ROOT definitions. This helps
+  to structure the load process of large collections of theories, and thus
+  reduce overall resource requirements.
 \<close>
 
 
diff -r 8abda6f6b700 -r 2071dbe5547d src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Mon Sep 30 13:11:22 2019 +0200
+++ b/src/Pure/Tools/dump.scala	Mon Sep 30 13:23:49 2019 +0200
@@ -88,6 +88,7 @@
     def apply(
       options: Options,
       logic: String,
+      dump_checkpoints: Boolean = false,
       aspects: List[Aspect] = Nil,
       progress: Progress = No_Progress,
       log: Logger = No_Logger,
@@ -95,13 +96,15 @@
       select_dirs: List[Path] = Nil,
       selection: Sessions.Selection = Sessions.Selection.empty): Session =
     {
-      new Session(options, logic, aspects, progress, log, dirs, select_dirs, selection)
+      new Session(
+        options, logic, dump_checkpoints, aspects, progress, log, dirs, select_dirs, selection)
     }
   }
 
   class Session private(
     options: Options,
     logic: String,
+    dump_checkpoints: Boolean,
     aspects: List[Aspect],
     progress: Progress,
     log: Logger,
@@ -214,7 +217,7 @@
             unicode_symbols = unicode_symbols,
             share_common_data = true,
             progress = progress,
-            checkpoints = deps.dump_checkpoints,
+            checkpoints = if (dump_checkpoints) deps.dump_checkpoints else Set.empty,
             commit = Some(Consumer.apply _))
 
         val bad_theories = Consumer.shutdown()
@@ -246,6 +249,7 @@
   def dump(
     options: Options,
     logic: String,
+    dump_checkpoints: Boolean = false,
     aspects: List[Aspect] = Nil,
     progress: Progress = No_Progress,
     log: Logger = No_Logger,
@@ -255,8 +259,9 @@
     selection: Sessions.Selection = Sessions.Selection.empty)
   {
     val session =
-      Session(options, logic, aspects = aspects, progress = progress, log = log,
-        dirs = dirs, select_dirs = select_dirs, selection = selection)
+      Session(options, logic, dump_checkpoints = dump_checkpoints, aspects = aspects,
+        progress = progress, log = log, dirs = dirs, select_dirs = select_dirs,
+        selection = selection)
 
     session.run((args: Args) =>
       {
@@ -277,6 +282,7 @@
       var aspects: List[Aspect] = known_aspects
       var base_sessions: List[String] = Nil
       var select_dirs: List[Path] = Nil
+      var dump_checkpoints = false
       var output_dir = default_output_dir
       var requirements = false
       var exclude_session_groups: List[String] = Nil
@@ -294,6 +300,7 @@
   Options are:
     -A NAMES     dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """)
     -B NAME      include session NAME and all descendants
+    -C           observe option dump_checkpoint for theories
     -D DIR       include session directory and select its sessions
     -O DIR       output directory for dumped files (default: """ + default_output_dir + """)
     -R           operate on requirements of selected sessions
@@ -311,6 +318,7 @@
 """ + Library.prefix_lines("    ", show_aspects) + "\n",
       "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
+      "C" -> (_ => dump_checkpoints = true),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
       "O:" -> (arg => output_dir = Path.explode(arg)),
       "R" -> (_ => requirements = true),
@@ -329,6 +337,7 @@
 
       progress.interrupt_handler {
         dump(options, logic,
+          dump_checkpoints = dump_checkpoints,
           aspects = aspects,
           progress = progress,
           dirs = dirs,