# HG changeset patch
# User wenzelm
# Date 1537533067 -7200
# Node ID fa7a1be0fab2d0e195099643e1db0b1c5b9efc64
# Parent  287bb00371c1b069cbb1cebd9b6308b09ef19a02
tuned signature;

diff -r 287bb00371c1 -r fa7a1be0fab2 src/Pure/Thy/sessions.scala
--- 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)
diff -r 287bb00371c1 -r fa7a1be0fab2 src/Pure/Tools/dump.scala
--- 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 */