tuned signature;
authorwenzelm
Tue, 18 Sep 2018 23:07:34 +0200
changeset 69014 a2c042364efc
parent 69013 bb4e4c253ebe
child 69015 5eb493b51bf6
tuned signature;
src/Pure/Thy/sessions.scala
src/Pure/Tools/dump.scala
--- a/src/Pure/Thy/sessions.scala	Tue Sep 18 11:14:30 2018 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Sep 18 23:07:34 2018 +0200
@@ -196,7 +196,7 @@
     def imported_sources(name: String): List[SHA1.Digest] =
       session_bases(name).imported_sources.map(_._2)
 
-    def used_theories_conditions(warning: String => Unit = _ => ()): List[String] =
+    def used_theories_condition(warning: String => Unit = _ => ()): List[Document.Node.Name] =
       for {
         session_name <- sessions_structure.build_topological_order
         (options, name) <- session_bases(session_name).used_theories
@@ -210,7 +210,7 @@
             false
           }
         }
-      } yield name.theory
+      } yield name
 
     def sources(name: String): List[SHA1.Digest] =
       session_bases(name).sources.map(_._2)
--- a/src/Pure/Tools/dump.scala	Tue Sep 18 11:14:30 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Tue Sep 18 23:07:34 2018 +0200
@@ -112,7 +112,7 @@
     val include_sessions =
       deps.sessions_structure.imports_topological_order
 
-    val use_theories = deps.used_theories_conditions(progress.echo_warning)
+    val use_theories = deps.used_theories_condition(progress.echo_warning).map(_.theory)
 
 
     /* dump aspects asynchronously */