more operations: record overall exported entities;
authorwenzelm
Wed, 04 Aug 2021 21:03:25 +0200
changeset 74119 342d0298e164
parent 74115 8752420f3377
child 74120 21ddf56ac140
more operations: record overall exported entities;
src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Wed Aug 04 21:00:37 2021 +0200
+++ b/src/Pure/Thy/export_theory.scala	Wed Aug 04 21:03:25 2021 +0200
@@ -92,6 +92,9 @@
       locales.iterator.map(_.no_content) ++
       locale_dependencies.iterator.map(_.no_content)
 
+    lazy val entity_serials: Set[Long] =
+      entity_iterator.map(_.serial).toSet
+
     def cache(cache: Term.Cache): Theory =
       Theory(cache.string(name),
         parents.map(cache.string),