--- a/src/Pure/Thy/sessions.scala Thu Aug 29 15:43:05 2019 +0200
+++ b/src/Pure/Thy/sessions.scala Thu Aug 29 17:13:49 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),