always export Pure theory;
authorwenzelm
Thu Aug 02 14:21:48 2018 +0200 (11 months ago)
changeset 687103db37e950118
parent 68709 6d9eca4805ff
child 68711 d1d03b7b6696
always export Pure theory;
src/Pure/ROOT
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/Pure/ROOT	Wed Aug 01 22:59:42 2018 +0100
     1.2 +++ b/src/Pure/ROOT	Thu Aug 02 14:21:48 2018 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4    description {*
     1.5      The Pure logical framework
     1.6    *}
     1.7 -  options [threads = 1]
     1.8 +  options [threads = 1, export_theory]
     1.9    theories
    1.10      Pure (global)
    1.11      ML_Bootstrap (global)
     2.1 --- a/src/Pure/Thy/export_theory.scala	Wed Aug 01 22:59:42 2018 +0100
     2.2 +++ b/src/Pure/Thy/export_theory.scala	Thu Aug 02 14:21:48 2018 +0200
     2.3 @@ -122,6 +122,20 @@
     2.4      if (cache.isDefined) theory.cache(cache.get) else theory
     2.5    }
     2.6  
     2.7 +  def read_pure_theory(store: Sessions.Store, cache: Term.Cache = Term.make_cache()): Theory =
     2.8 +  {
     2.9 +    val session_name = Thy_Header.PURE
    2.10 +    val theory_name = Thy_Header.PURE
    2.11 +
    2.12 +    using(store.open_database(session_name))(db =>
    2.13 +    {
    2.14 +      db.transaction {
    2.15 +        read_theory(Export.Provider.database(db, session_name, theory_name),
    2.16 +          session_name, theory_name, cache = Some(cache))
    2.17 +      }
    2.18 +    })
    2.19 +  }
    2.20 +
    2.21  
    2.22    /* entities */
    2.23