tuned signature;
authorwenzelm
Thu Aug 02 21:49:31 2018 +0200 (11 months ago)
changeset 68711d1d03b7b6696
parent 68710 3db37e950118
child 68712 fc51dcb4e6fd
tuned signature;
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/Pure/Thy/export_theory.scala	Thu Aug 02 14:21:48 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.scala	Thu Aug 02 21:49:31 2018 +0200
     1.3 @@ -75,6 +75,14 @@
     1.4    {
     1.5      override def toString: String = name
     1.6  
     1.7 +    lazy val entities: Set[Long] =
     1.8 +      Set.empty[Long] ++
     1.9 +        types.iterator.map(_.entity.serial) ++
    1.10 +        consts.iterator.map(_.entity.serial) ++
    1.11 +        axioms.iterator.map(_.entity.serial) ++
    1.12 +        facts.iterator.map(_.entity.serial) ++
    1.13 +        classes.iterator.map(_.entity.serial)
    1.14 +
    1.15      def cache(cache: Term.Cache): Theory =
    1.16        Theory(cache.string(name),
    1.17          parents.map(cache.string(_)),
    1.18 @@ -122,7 +130,7 @@
    1.19      if (cache.isDefined) theory.cache(cache.get) else theory
    1.20    }
    1.21  
    1.22 -  def read_pure_theory(store: Sessions.Store, cache: Term.Cache = Term.make_cache()): Theory =
    1.23 +  def read_pure_theory(store: Sessions.Store, cache: Option[Term.Cache] = None): Theory =
    1.24    {
    1.25      val session_name = Thy_Header.PURE
    1.26      val theory_name = Thy_Header.PURE
    1.27 @@ -131,7 +139,7 @@
    1.28      {
    1.29        db.transaction {
    1.30          read_theory(Export.Provider.database(db, session_name, theory_name),
    1.31 -          session_name, theory_name, cache = Some(cache))
    1.32 +          session_name, theory_name, cache = cache)
    1.33        }
    1.34      })
    1.35    }