--- 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)