# HG changeset patch
# User wenzelm
# Date 1567515403 -7200
# Node ID fc27cecb66d871e2681b493161e4c27ae8299713
# Parent  b23a6dfcfd5742fc1b8012a3c294f2f790f3cef7
clarified signature;

diff -r b23a6dfcfd57 -r fc27cecb66d8 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Sep 03 11:32:29 2019 +0200
+++ b/src/Pure/PIDE/resources.scala	Tue Sep 03 14:56:43 2019 +0200
@@ -135,12 +135,12 @@
   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
+  def dump_checkpoints(info: Sessions.Info): Set[Document.Node.Name] =
+    (for {
+      (options, thys) <- info.theories.iterator
       if options.bool("dump_checkpoint")
-      (thy, _) <- thys
-    } yield import_name(info, thy)
+      (thy, _) <- thys.iterator
+    } yield import_name(info, thy)).toSet
 
   def standard_import(base: Sessions.Base, qualifier: String, dir: String, s: String): String =
   {
diff -r b23a6dfcfd57 -r fc27cecb66d8 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Sep 03 11:32:29 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Sep 03 14:56:43 2019 +0200
@@ -148,7 +148,7 @@
     global_theories: Map[String, String] = Map.empty,
     loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
     used_theories: List[((Document.Node.Name, Options), List[Document.Node.Name])] = Nil,
-    dump_checkpoint: List[Document.Node.Name] = Nil,
+    dump_checkpoints: Set[Document.Node.Name] = Set.empty,
     known: Known = Known.empty,
     overall_syntax: Outer_Syntax = Outer_Syntax.empty,
     imported_sources: List[(Path, SHA1.Digest)] = Nil,
@@ -201,11 +201,11 @@
     def imported_sources(name: String): List[SHA1.Digest] =
       session_bases(name).imported_sources.map(_._2)
 
-    def dump_checkpoint: List[Document.Node.Name] =
+    def dump_checkpoints: Set[Document.Node.Name] =
       (for {
         (_, base) <- session_bases.iterator
-        name <- base.dump_checkpoint.iterator
-      } yield name).toList
+        name <- base.dump_checkpoints.iterator
+      } yield name).toSet
 
     def used_theories_condition(default_options: Options, progress: Progress = No_Progress)
       : Graph[Document.Node.Name, Options] =
@@ -311,7 +311,7 @@
 
             val dependencies = resources.session_dependencies(info)
 
-            val dump_checkpoint = resources.dump_checkpoint(info)
+            val dump_checkpoints = resources.dump_checkpoints(info)
 
             val overall_syntax = dependencies.overall_syntax
 
@@ -393,7 +393,7 @@
                 global_theories = global_theories,
                 loaded_theories = dependencies.loaded_theories,
                 used_theories = used_theories,
-                dump_checkpoint = dump_checkpoint,
+                dump_checkpoints = dump_checkpoints,
                 known = known,
                 overall_syntax = overall_syntax,
                 imported_sources = check_sources(imported_files),
diff -r b23a6dfcfd57 -r fc27cecb66d8 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Tue Sep 03 11:32:29 2019 +0200
+++ b/src/Pure/Tools/dump.scala	Tue Sep 03 14:56:43 2019 +0200
@@ -209,10 +209,10 @@
       // run
 
       try {
-        val dump_checkpoint = deps.dump_checkpoint.toSet
+        val dump_checkpoints = deps.dump_checkpoints
         def commit(snapshot: Document.Snapshot, status: Document_Status.Node_Status)
         {
-          if (dump_checkpoint(snapshot.node_name)) {
+          if (dump_checkpoints.contains(snapshot.node_name)) {
             session.protocol_command("ML_Heap.share_common_data")
           }
           Consumer.apply(snapshot, status)