src/Pure/Thy/sessions.scala
changeset 70796 2739631ac368
parent 70788 b254a95b6e77
child 70859 6e6254bbce1f
--- a/src/Pure/Thy/sessions.scala	Mon Oct 07 10:51:20 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Oct 07 11:35:43 2019 +0200
@@ -54,7 +54,6 @@
     global_theories: Map[String, String] = Map.empty,
     loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
     used_theories: List[(Document.Node.Name, Options)] = Nil,
-    dump_checkpoints: Set[Document.Node.Name] = Set.empty,
     known_theories: Map[String, Document.Node.Entry] = Map.empty,
     known_loaded_files: Map[String, List[Path]] = Map.empty,
     overall_syntax: Outer_Syntax = Outer_Syntax.empty,
@@ -98,12 +97,6 @@
     def imported_sources(name: String): List[SHA1.Digest] =
       session_bases(name).imported_sources.map(_._2)
 
-    def dump_checkpoints: Set[Document.Node.Name] =
-      (for {
-        (_, base) <- session_bases.iterator
-        name <- base.dump_checkpoints.iterator
-      } yield name).toSet
-
     def used_theories_condition(default_options: Options, progress: Progress = No_Progress)
       : List[(Document.Node.Name, Options)] =
     {
@@ -219,8 +212,6 @@
 
             val dependencies = resources.session_dependencies(info)
 
-            val dump_checkpoints = resources.dump_checkpoints(info)
-
             val overall_syntax = dependencies.overall_syntax
 
             val theory_files = dependencies.theories.map(_.path)
@@ -338,7 +329,6 @@
                 global_theories = sessions_structure.global_theories,
                 loaded_theories = dependencies.loaded_theories,
                 used_theories = used_theories,
-                dump_checkpoints = dump_checkpoints,
                 known_theories = known_theories,
                 known_loaded_files = known_loaded_files,
                 overall_syntax = overall_syntax,