# HG changeset patch # User wenzelm # Date 1537304854 -7200 # Node ID a2c042364efcab01d4d60a63422f279d157755bb # Parent bb4e4c253ebe78fc862e3841f038ace5ecb3ff94 tuned signature; diff -r bb4e4c253ebe -r a2c042364efc src/Pure/Thy/sessions.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) diff -r bb4e4c253ebe -r a2c042364efc src/Pure/Tools/dump.scala --- 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 */