--- a/src/Pure/Thy/sessions.scala Thu Sep 20 23:05:18 2018 +0200
+++ b/src/Pure/Thy/sessions.scala Fri Sep 21 14:31:07 2018 +0200
@@ -196,7 +196,9 @@
def imported_sources(name: String): List[SHA1.Digest] =
session_bases(name).imported_sources.map(_._2)
- def used_theories_condition(warning: String => Unit = _ => ()): List[Document.Node.Name] =
+ def used_theories_condition(warning: String => Unit = _ => ())
+ : List[(Options, Document.Node.Name)] =
+ {
for {
session_name <- sessions_structure.build_topological_order
(options, name) <- session_bases(session_name).used_theories
@@ -210,7 +212,8 @@
false
}
}
- } yield name
+ } yield (options, name)
+ }
def sources(name: String): List[SHA1.Digest] =
session_bases(name).sources.map(_._2)
--- a/src/Pure/Tools/dump.scala Thu Sep 20 23:05:18 2018 +0200
+++ b/src/Pure/Tools/dump.scala Fri Sep 21 14:31:07 2018 +0200
@@ -112,7 +112,9 @@
val include_sessions =
deps.sessions_structure.imports_topological_order
- val use_theories = deps.used_theories_condition(progress.echo_warning).map(_.theory)
+ val use_theories =
+ for { (_, name) <- deps.used_theories_condition(progress.echo_warning) }
+ yield name.theory
/* dump aspects asynchronously */