merged

--- a/etc/options	Thu Aug 29 19:07:09 2019 +0200
+++ b/etc/options	Sat Aug 31 21:34:39 2019 +0200
@@ -219,6 +219,9 @@
 option execution_eager : bool = false
   -- "prefer theories with shorter stack of decendants"
 
+option dump_checkpoint : bool = false
+  -- "mark individual theories to share common data in ML"
+
 
 section "Miscellaneous Tools"
 

--- a/src/HOL/ROOT	Thu Aug 29 19:07:09 2019 +0200
+++ b/src/HOL/ROOT	Sat Aug 31 21:34:39 2019 +0200
@@ -5,7 +5,7 @@
     Classical Higher-order Logic.
   "
   options [strict_facts]
-  theories
+  theories [dump_checkpoint]
     Main (global)
     Complex_Main (global)
   document_files
@@ -64,7 +64,7 @@
   sessions
     "HOL-Library"
     "HOL-Computational_Algebra"
-  theories
+  theories [dump_checkpoint]
     Analysis
   document_files
     "root.tex"

--- a/src/Pure/PIDE/resources.scala	Thu Aug 29 19:07:09 2019 +0200
+++ b/src/Pure/PIDE/resources.scala	Sat Aug 31 21:34:39 2019 +0200
@@ -132,6 +132,16 @@
   def import_name(name: Document.Node.Name, s: String): Document.Node.Name =
     import_name(session_base.theory_qualifier(name), name.master_dir, s)
 
+  def import_name(info: Sessions.Info, s: String): Document.Node.Name =
+    import_name(info.name, info.dir.implode, s)
+
+  def dump_checkpoint(info: Sessions.Info): List[Document.Node.Name] =
+    for {
+      (options, thys) <- info.theories
+      if options.bool("dump_checkpoint")
+      (thy, _) <- thys
+    } yield import_name(info, thy)
+
   def standard_import(base: Sessions.Base, qualifier: String, dir: String, s: String): String =
   {
     val name = import_name(qualifier, dir, s)
@@ -246,12 +256,9 @@
   def session_dependencies(info: Sessions.Info, progress: Progress = No_Progress)
     : Dependencies[Options] =
   {
-    val qualifier = info.name
-    val dir = info.dir.implode
-
     (Dependencies.empty[Options] /: info.theories)({ case (dependencies, (options, thys)) =>
       dependencies.require_thys(options,
-        for { (thy, pos) <- thys } yield (import_name(qualifier, dir, thy), pos),
+        for { (thy, pos) <- thys } yield (import_name(info, thy), pos),
         progress = progress)
     })
   }

--- a/src/Pure/Thy/sessions.scala	Thu Aug 29 19:07:09 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Aug 31 21:34:39 2019 +0200
@@ -148,6 +148,7 @@
     global_theories: Map[String, String] = Map.empty,
     loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
     used_theories: List[(Options, Document.Node.Name)] = Nil,
+    dump_checkpoint: List[Document.Node.Name] = Nil,
     known: Known = Known.empty,
     overall_syntax: Outer_Syntax = Outer_Syntax.empty,
     imported_sources: List[(Path, SHA1.Digest)] = Nil,
@@ -200,6 +201,12 @@
     def imported_sources(name: String): List[SHA1.Digest] =
       session_bases(name).imported_sources.map(_._2)
 
+    def dump_checkpoint: List[Document.Node.Name] =
+      (for {
+        (_, base) <- session_bases.iterator
+        name <- base.dump_checkpoint.iterator
+      } yield name).toList
+
     def used_theories_condition(default_options: Options, progress: Progress = No_Progress)
       : List[(Options, Document.Node.Name)] =
     {
@@ -301,6 +308,8 @@
 
             val dependencies = resources.session_dependencies(info)
 
+            val dump_checkpoint = resources.dump_checkpoint(info)
+
             val overall_syntax = dependencies.overall_syntax
 
             val theory_files = dependencies.theories.map(_.path)
@@ -379,6 +388,7 @@
                 global_theories = global_theories,
                 loaded_theories = dependencies.loaded_theories,
                 used_theories = dependencies.adjunct_theories,
+                dump_checkpoint = dump_checkpoint,
                 known = known,
                 overall_syntax = overall_syntax,
                 imported_sources = check_sources(imported_files),

--- a/src/Pure/Tools/dump.scala	Thu Aug 29 19:07:09 2019 +0200
+++ b/src/Pure/Tools/dump.scala	Sat Aug 31 21:34:39 2019 +0200
@@ -167,13 +167,22 @@
     /* run session */
 
     try {
+      val dump_checkpoint = deps.dump_checkpoint.toSet
+      def commit(snapshot: Document.Snapshot, status: Document_Status.Node_Status)
+      {
+        if (dump_checkpoint(snapshot.node_name)) {
+          session.protocol_command("ML_Heap.share_common_data")
+        }
+        Consumer.apply(snapshot, status)
+      }
+
       val use_theories = resources.used_theories(deps).map(_.theory)
       val use_theories_result =
         session.use_theories(use_theories,
           unicode_symbols = unicode_symbols,
           share_common_data = true,
           progress = progress,
-          commit = Some(Consumer.apply _))
+          commit = Some(commit _))
 
       val bad_theories = Consumer.shutdown()
       val bad_msgs =

--- a/src/ZF/ROOT	Thu Aug 29 19:07:09 2019 +0200
+++ b/src/ZF/ROOT	Sat Aug 31 21:34:39 2019 +0200
@@ -46,6 +46,7 @@
     FOL
   theories
     ZF (global)
+  theories [dump_checkpoint]
     ZFC (global)
   document_files "root.tex"