# HG changeset patch # User wenzelm # Date 1609599528 -3600 # Node ID 337e1b135d2f7f39829dda5a34f433238e498563 # Parent e15621aa8c72324e4815a391753379406dc167a5 clarified signature --- internal Cache.none; diff -r e15621aa8c72 -r 337e1b135d2f src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Sat Jan 02 14:24:03 2021 +0100 +++ b/src/Pure/Admin/build_log.scala Sat Jan 02 15:58:48 2021 +0100 @@ -244,7 +244,7 @@ /* properties (YXML) */ - val xml_cache: XML.Cache = XML.make_cache() + val xml_cache: XML.Cache = XML.Cache.make() def parse_props(text: String): Properties.T = try { xml_cache.props(XML.Decode.properties(YXML.parse_body(text))) } @@ -648,14 +648,14 @@ errors = log_file.filter(Protocol.Error_Message_Marker)) } - def compress_errors(errors: List[String], cache: XZ.Cache = XZ.cache()): Option[Bytes] = + def compress_errors(errors: List[String], cache: XZ.Cache = XZ.Cache()): Option[Bytes] = if (errors.isEmpty) None else { Some(Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.string)(errors))). compress(cache = cache)) } - def uncompress_errors(bytes: Bytes, cache: XZ.Cache = XZ.cache()): List[String] = + def uncompress_errors(bytes: Bytes, cache: XZ.Cache = XZ.Cache()): List[String] = if (bytes.is_empty) Nil else { XML.Decode.list(YXML.string_of_body)(YXML.parse_body(bytes.uncompress(cache = cache).text)) @@ -850,13 +850,16 @@ /* database access */ - def store(options: Options): Store = new Store(options) + def store(options: Options, + xml_cache: XML.Cache = XML.Cache.make(), + xz_cache: XZ.Cache = XZ.Cache.make()): Store = + new Store(options, xml_cache, xz_cache) - class Store private[Build_Log](options: Options) + class Store private[Build_Log]( + options: Options, + val xml_cache: XML.Cache, + val xz_cache: XZ.Cache) { - val xml_cache: XML.Cache = XML.make_cache() - val xz_cache: XZ.Cache = XZ.make_cache() - def open_database( user: String = options.string("build_log_database_user"), password: String = options.string("build_log_database_password"), @@ -1164,7 +1167,7 @@ ml_statistics = if (ml_statistics) { Properties.uncompress( - res.bytes(Data.ml_statistics), cache = xz_cache, Some(xml_cache)) + res.bytes(Data.ml_statistics), cache = xz_cache, xml_cache = xml_cache) } else Nil) session_name -> session_entry diff -r e15621aa8c72 -r 337e1b135d2f src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Sat Jan 02 14:24:03 2021 +0100 +++ b/src/Pure/General/bytes.scala Sat Jan 02 15:58:48 2021 +0100 @@ -195,17 +195,17 @@ /* XZ data compression */ - def uncompress(cache: XZ.Cache = XZ.cache()): Bytes = + def uncompress(cache: XZ.Cache = XZ.Cache()): Bytes = using(new XZInputStream(stream(), cache))(Bytes.read_stream(_, hint = length)) - def compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.cache()): Bytes = + def compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.Cache()): Bytes = { val result = new ByteArrayOutputStream(length) using(new XZOutputStream(result, options, cache))(write_stream(_)) new Bytes(result.toByteArray, 0, result.size) } - def maybe_compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.cache()) + def maybe_compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.Cache()) : (Boolean, Bytes) = { val compressed = compress(options = options, cache = cache) diff -r e15621aa8c72 -r 337e1b135d2f src/Pure/General/cache.scala --- a/src/Pure/General/cache.scala Sat Jan 02 14:24:03 2021 +0100 +++ b/src/Pure/General/cache.scala Sat Jan 02 15:58:48 2021 +0100 @@ -7,30 +7,49 @@ package isabelle -import java.util.{Collections, WeakHashMap} +import java.util.{Collections, WeakHashMap, Map => JMap} import java.lang.ref.WeakReference -class Cache(initial_size: Int = 131071, max_string: Int = 100) +object Cache { - private val table = - Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size)) + val default_max_string = 100 + val default_initial_size = 131071 + + def make(max_string: Int = default_max_string, initial_size: Int = default_initial_size): Cache = + new Cache(max_string, initial_size) + + val none: Cache = make(max_string = 0) +} - def size: Int = table.size +class Cache(max_string: Int, initial_size: Int) +{ + val no_cache: Boolean = max_string == 0 - override def toString: String = "Cache(" + size + ")" + private val table: JMap[Any, WeakReference[Any]] = + if (max_string == 0) null + else Collections.synchronizedMap(new WeakHashMap[Any, WeakReference[Any]](initial_size)) + + override def toString: String = + if (no_cache) "Cache.none" else "Cache(size = " + table.size + ")" protected def lookup[A](x: A): Option[A] = { - val ref = table.get(x) - if (ref == null) None - else Option(ref.asInstanceOf[WeakReference[A]].get) + if (table == null) None + else { + val ref = table.get(x) + if (ref == null) None + else Option(ref.asInstanceOf[WeakReference[A]].get) + } } protected def store[A](x: A): A = { - table.put(x, new WeakReference[Any](x)) - x + if (table == null) x + else { + table.put(x, new WeakReference[Any](x)) + x + } } protected def cache_string(x: String): String = @@ -51,5 +70,6 @@ } // main methods - def string(x: String): String = synchronized { cache_string(x) } + def string(x: String): String = + if (no_cache) x else synchronized { cache_string(x) } } diff -r e15621aa8c72 -r 337e1b135d2f src/Pure/General/properties.scala --- a/src/Pure/General/properties.scala Sat Jan 02 14:24:03 2021 +0100 +++ b/src/Pure/General/properties.scala Sat Jan 02 15:58:48 2021 +0100 @@ -37,18 +37,12 @@ def encode(ps: T): Bytes = Bytes(YXML.string_of_body(XML.Encode.properties(ps))) - def decode(bs: Bytes, xml_cache: Option[XML.Cache] = None): T = - { - val ps = XML.Decode.properties(YXML.parse_body(bs.text)) - xml_cache match { - case None => ps - case Some(cache) => cache.props(ps) - } - } + def decode(bs: Bytes, xml_cache: XML.Cache = XML.Cache.none): T = + xml_cache.props(XML.Decode.properties(YXML.parse_body(bs.text))) def compress(ps: List[T], options: XZ.Options = XZ.options(), - cache: XZ.Cache = XZ.cache()): Bytes = + cache: XZ.Cache = XZ.Cache()): Bytes = { if (ps.isEmpty) Bytes.empty else { @@ -58,17 +52,14 @@ } def uncompress(bs: Bytes, - cache: XZ.Cache = XZ.cache(), - xml_cache: Option[XML.Cache] = None): List[T] = + cache: XZ.Cache = XZ.Cache(), + xml_cache: XML.Cache = XML.Cache.none): List[T] = { if (bs.is_empty) Nil else { val ps = XML.Decode.list(XML.Decode.properties)(YXML.parse_body(bs.uncompress(cache = cache).text)) - xml_cache match { - case None => ps - case Some(cache) => ps.map(cache.props) - } + if (xml_cache.no_cache) ps else ps.map(xml_cache.props) } } diff -r e15621aa8c72 -r 337e1b135d2f src/Pure/General/xz.scala --- a/src/Pure/General/xz.scala Sat Jan 02 14:24:03 2021 +0100 +++ b/src/Pure/General/xz.scala Sat Jan 02 15:58:48 2021 +0100 @@ -28,7 +28,10 @@ type Cache = ArrayCache - def no_cache(): ArrayCache = ArrayCache.getDummyCache() - def cache(): ArrayCache = ArrayCache.getDefaultCache() - def make_cache(): ArrayCache = new BasicArrayCache + object Cache + { + def none: ArrayCache = ArrayCache.getDummyCache() + def apply(): ArrayCache = ArrayCache.getDefaultCache() + def make(): ArrayCache = new BasicArrayCache + } } diff -r e15621aa8c72 -r 337e1b135d2f src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Sat Jan 02 14:24:03 2021 +0100 +++ b/src/Pure/PIDE/session.scala Sat Jan 02 15:58:48 2021 +0100 @@ -127,8 +127,8 @@ { session => - val xml_cache: XML.Cache = XML.make_cache() - val xz_cache: XZ.Cache = XZ.make_cache() + val xml_cache: XML.Cache = XML.Cache.make() + val xz_cache: XZ.Cache = XZ.Cache.make() def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = Command.Blobs_Info.none diff -r e15621aa8c72 -r 337e1b135d2f src/Pure/PIDE/xml.scala --- a/src/Pure/PIDE/xml.scala Sat Jan 02 14:24:03 2021 +0100 +++ b/src/Pure/PIDE/xml.scala Sat Jan 02 15:58:48 2021 +0100 @@ -170,11 +170,18 @@ /** cache **/ - def make_cache(initial_size: Int = 131071, max_string: Int = 100): Cache = - new Cache(initial_size, max_string) + object Cache + { + def make( + max_string: Int = isabelle.Cache.default_max_string, + initial_size: Int = isabelle.Cache.default_initial_size): Cache = + new Cache(max_string, initial_size) - class Cache private[XML](initial_size: Int, max_string: Int) - extends isabelle.Cache(initial_size, max_string) + val none: Cache = make(max_string = 0) + } + + class Cache private[XML](max_string: Int, initial_size: Int) + extends isabelle.Cache(max_string, initial_size) { protected def cache_props(x: Properties.T): Properties.T = { @@ -222,11 +229,16 @@ } // main methods - def props(x: Properties.T): Properties.T = synchronized { cache_props(x) } - def markup(x: Markup): Markup = synchronized { cache_markup(x) } - def tree(x: XML.Tree): XML.Tree = synchronized { cache_tree(x) } - def body(x: XML.Body): XML.Body = synchronized { cache_body(x) } - def elem(x: XML.Elem): XML.Elem = synchronized { cache_tree(x).asInstanceOf[XML.Elem] } + def props(x: Properties.T): Properties.T = + if (no_cache) x else synchronized { cache_props(x) } + def markup(x: Markup): Markup = + if (no_cache) x else synchronized { cache_markup(x) } + def tree(x: XML.Tree): XML.Tree = + if (no_cache) x else synchronized { cache_tree(x) } + def body(x: XML.Body): XML.Body = + if (no_cache) x else synchronized { cache_body(x) } + def elem(x: XML.Elem): XML.Elem = + if (no_cache) x else synchronized { cache_tree(x).asInstanceOf[XML.Elem] } } diff -r e15621aa8c72 -r 337e1b135d2f src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Sat Jan 02 14:24:03 2021 +0100 +++ b/src/Pure/Thy/export.scala Sat Jan 02 15:58:48 2021 +0100 @@ -85,7 +85,7 @@ def compound_name(a: String, b: String): String = a + ":" + b def empty_entry(theory_name: String, name: String): Entry = - Entry("", theory_name, name, false, Future.value(false, Bytes.empty), XZ.no_cache()) + Entry("", theory_name, name, false, Future.value(false, Bytes.empty), XZ.Cache.none) sealed case class Entry( session_name: String, diff -r e15621aa8c72 -r 337e1b135d2f src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala Sat Jan 02 14:24:03 2021 +0100 +++ b/src/Pure/Thy/export_theory.scala Sat Jan 02 15:58:48 2021 +0100 @@ -31,7 +31,7 @@ sessions_structure: Sessions.Structure, session_name: String, progress: Progress = new Progress, - cache: Term.Cache = Term.make_cache()): Session = + cache: Term.Cache = Term.Cache.make()): Session = { val thys = sessions_structure.build_requirements(List(session_name)).flatMap(session => @@ -42,7 +42,7 @@ yield { progress.echo("Reading theory " + theory) read_theory(Export.Provider.database(db, store.xz_cache, session, theory), - session, theory, cache = Some(cache)) + session, theory, cache = cache) } } })) @@ -107,7 +107,7 @@ } def read_theory(provider: Export.Provider, session_name: String, theory_name: String, - cache: Option[Term.Cache] = None): Theory = + cache: Term.Cache = Term.Cache.none): Theory = { val parents = if (theory_name == Thy_Header.PURE) Nil @@ -134,7 +134,7 @@ read_typedefs(provider), read_datatypes(provider), read_spec_rules(provider)) - if (cache.isDefined) theory.cache(cache.get) else theory + if (cache.no_cache) theory else theory.cache(cache) } def read_pure[A](store: Sessions.Store, read: (Export.Provider, String, String) => A): A = @@ -151,11 +151,11 @@ }) } - def read_pure_theory(store: Sessions.Store, cache: Option[Term.Cache] = None): Theory = + def read_pure_theory(store: Sessions.Store, cache: Term.Cache = Term.Cache.none): Theory = read_pure(store, read_theory(_, _, _, cache = cache)) def read_pure_proof( - store: Sessions.Store, id: Thm_Id, cache: Option[Term.Cache] = None): Option[Proof] = + store: Sessions.Store, id: Thm_Id, cache: Term.Cache = Term.Cache.none): Option[Proof] = read_pure(store, (provider, _, _) => read_proof(provider, id, cache = cache)) @@ -375,7 +375,7 @@ } def read_proof( - provider: Export.Provider, id: Thm_Id, cache: Option[Term.Cache] = None): Option[Proof] = + provider: Export.Provider, id: Thm_Id, cache: Term.Cache = Term.Cache.none): Option[Proof] = { for { entry <- provider.focus(id.theory_name)(Export.PROOFS_PREFIX + id.serial) } yield { @@ -391,7 +391,7 @@ val proof = Term_XML.Decode.proof_env(env)(proof_body) val result = Proof(typargs, args, prop, proof) - cache.map(result.cache(_)) getOrElse result + if (cache.no_cache) result else result.cache(cache) } } @@ -400,7 +400,7 @@ provider: Export.Provider, proof: Term.Proof, suppress: Thm_Id => Boolean = _ => false, - cache: Option[Term.Cache] = None): List[(Thm_Id, Proof)] = + cache: Term.Cache = Term.Cache.none): List[(Thm_Id, Proof)] = { var seen = Set.empty[Long] var result = SortedMap.empty[Long, (Thm_Id, Proof)] diff -r e15621aa8c72 -r 337e1b135d2f src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Sat Jan 02 14:24:03 2021 +0100 +++ b/src/Pure/Thy/sessions.scala Sat Jan 02 15:58:48 2021 +0100 @@ -1259,17 +1259,20 @@ } } - def store(options: Options): Store = new Store(options) + def store(options: Options, + xml_cache: XML.Cache = XML.Cache.make(), + xz_cache: XZ.Cache = XZ.Cache.make()): Store = + new Store(options, xml_cache, xz_cache) - class Store private[Sessions](val options: Options) + class Store private[Sessions]( + val options: Options, + val xml_cache: XML.Cache, + val xz_cache: XZ.Cache) { store => override def toString: String = "Store(output_dir = " + output_dir.absolute + ")" - val xml_cache: XML.Cache = XML.make_cache() - val xz_cache: XZ.Cache = XZ.make_cache() - /* directories */ @@ -1405,7 +1408,7 @@ def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] = Properties.uncompress( - read_bytes(db, name, column), cache = xz_cache, xml_cache = Some(xml_cache)) + read_bytes(db, name, column), cache = xz_cache, xml_cache = xml_cache) /* session info */ @@ -1471,7 +1474,7 @@ } def read_session_timing(db: SQL.Database, name: String): Properties.T = - Properties.decode(read_bytes(db, name, Session_Info.session_timing), Some(xml_cache)) + Properties.decode(read_bytes(db, name, Session_Info.session_timing), xml_cache = xml_cache) def read_command_timings(db: SQL.Database, name: String): List[Properties.T] = read_properties(db, name, Session_Info.command_timings) diff -r e15621aa8c72 -r 337e1b135d2f src/Pure/term.scala --- a/src/Pure/term.scala Sat Jan 02 14:24:03 2021 +0100 +++ b/src/Pure/term.scala Sat Jan 02 15:58:48 2021 +0100 @@ -133,17 +133,25 @@ /** cache **/ - def make_cache(initial_size: Int = 131071, max_string: Int = Integer.MAX_VALUE): Cache = - new Cache(initial_size, max_string) + object Cache + { + def make( + max_string: Int = Integer.MAX_VALUE, + initial_size: Int = isabelle.Cache.default_initial_size): Cache = + new Cache(initial_size, max_string) - class Cache private[Term](initial_size: Int, max_string: Int) - extends isabelle.Cache(initial_size, max_string) + val none: Cache = make(max_string = 0) + } + + class Cache private[Term](max_string: Int, initial_size: Int) + extends isabelle.Cache(max_string = max_string, initial_size = initial_size) { protected def cache_indexname(x: Indexname): Indexname = lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index)) protected def cache_sort(x: Sort): Sort = - if (x.isEmpty) Nil else lookup(x) getOrElse store(x.map(cache_string)) + if (x.isEmpty) Nil + else lookup(x) getOrElse store(x.map(cache_string)) protected def cache_typ(x: Typ): Typ = { @@ -216,13 +224,19 @@ } // main methods - def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) } - def sort(x: Sort): Sort = synchronized { cache_sort(x) } - def typ(x: Typ): Typ = synchronized { cache_typ(x) } - def term(x: Term): Term = synchronized { cache_term(x) } - def proof(x: Proof): Proof = synchronized { cache_proof(x) } + def indexname(x: Indexname): Indexname = + if (no_cache) x else synchronized { cache_indexname(x) } + def sort(x: Sort): Sort = + if (no_cache) x else synchronized { cache_sort(x) } + def typ(x: Typ): Typ = + if (no_cache) x else synchronized { cache_typ(x) } + def term(x: Term): Term = + if (no_cache) x else synchronized { cache_term(x) } + def proof(x: Proof): Proof = + if (no_cache) x else synchronized { cache_proof(x) } def position(x: Position.T): Position.T = - synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) } + if (no_cache) x + else synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) } } }