# HG changeset patch
# User wenzelm
# Date 1571084526 -7200
# Node ID 2beac4adc565a192c2f353a859b9aafb9fbbe0f7
# Parent  877fe56af1787394278d886fe997a3208f2a9eed
more complete coverage of sessions: process_theory operation needs to handle duplicate theories;

diff -r 877fe56af178 -r 2beac4adc565 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Mon Oct 14 22:09:10 2019 +0200
+++ b/src/Pure/Tools/dump.scala	Mon Oct 14 22:22:06 2019 +0200
@@ -227,11 +227,6 @@
     private def deps = context.deps
     private def progress = context.progress
 
-    private val selected_session = selected_sessions.toSet
-
-    private def selected_theory(name: Document.Node.Name): Boolean =
-      selected_session(deps.sessions_structure.theory_qualifier(name.theory))
-
     val resources: Headless.Resources =
       Headless.Resources.make(options, logic, progress = progress, log = log,
         session_dirs = context.session_dirs,
@@ -241,7 +236,7 @@
     {
       for {
         session_name <-
-          deps.sessions_structure.build_graph.restrict(selected_session).topological_order
+          deps.sessions_structure.build_graph.restrict(selected_sessions.toSet).topological_order
         (name, theory_options) <- deps(session_name).used_theories
         if !resources.session_base.loaded_theory(name.theory)
         if {
@@ -289,28 +284,26 @@
               {
                 val (snapshot, status) = args
                 val name = snapshot.node_name
-                if (selected_theory(name)) {
-                  if (status.ok) {
-                    try { process_theory(Args(session, snapshot, status)) }
-                    catch {
-                      case exn: Throwable if !Exn.is_interrupt(exn) =>
-                        val msg = Exn.message(exn)
-                        progress.echo("FAILED to process theory " + name)
-                        progress.echo_error_message(msg)
-                        consumer_bad_theories.change(Bad_Theory(name, status, List(msg)) :: _)
-                    }
+                if (status.ok) {
+                  try { process_theory(Args(session, snapshot, status)) }
+                  catch {
+                    case exn: Throwable if !Exn.is_interrupt(exn) =>
+                      val msg = Exn.message(exn)
+                      progress.echo("FAILED to process theory " + name)
+                      progress.echo_error_message(msg)
+                      consumer_bad_theories.change(Bad_Theory(name, status, List(msg)) :: _)
                   }
-                  else {
-                    val msgs =
-                      for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree))
-                      yield {
-                        "Error" + Position.here(pos) + ":\n" +
-                          XML.content(Pretty.formatted(List(tree)))
-                      }
-                    progress.echo("FAILED to process theory " + name)
-                    msgs.foreach(progress.echo_error_message)
-                    consumer_bad_theories.change(Bad_Theory(name, status, msgs) :: _)
-                  }
+                }
+                else {
+                  val msgs =
+                    for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree))
+                    yield {
+                      "Error" + Position.here(pos) + ":\n" +
+                        XML.content(Pretty.formatted(List(tree)))
+                    }
+                  progress.echo("FAILED to process theory " + name)
+                  msgs.foreach(progress.echo_error_message)
+                  consumer_bad_theories.change(Bad_Theory(name, status, msgs) :: _)
                 }
                 true
               })