# HG changeset patch
# User wenzelm
# Date 1571130378 -7200
# Node ID a62c34770df94c60dc2ea18eb89963312a976b2d
# Parent  2010397f7c9a794b6cef7233f728d898a24454af
proper guard for process_theory: ensure uniform precedence of results;

diff -r 2010397f7c9a -r a62c34770df9 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Tue Oct 15 10:52:42 2019 +0200
+++ b/src/Pure/Tools/dump.scala	Tue Oct 15 11:06:18 2019 +0200
@@ -209,6 +209,14 @@
 
       proofs ::: base ::: main ::: afp
     }
+
+
+    /* processed theories */
+
+    private val processed_theories = Synchronized(Set.empty[String])
+
+    def process_theory(theory: String): Boolean =
+      processed_theories.change_result(processed => (!processed(theory), processed + theory))
   }
 
   class Session private[Dump](
@@ -285,7 +293,11 @@
                 val (snapshot, status) = args
                 val name = snapshot.node_name
                 if (status.ok) {
-                  try { process_theory(Args(session, snapshot, status)) }
+                  try {
+                    if (context.process_theory(name.theory)) {
+                      process_theory(Args(session, snapshot, status))
+                    }
+                  }
                   catch {
                     case exn: Throwable if !Exn.is_interrupt(exn) =>
                       val msg = Exn.message(exn)