--- a/src/Pure/Admin/build_log.scala Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/Admin/build_log.scala Sat Jan 02 22:22:34 2021 +0100
@@ -244,10 +244,10 @@
/* properties (YXML) */
- val xml_cache: XML.Cache = XML.Cache.make()
+ val cache: XML.Cache = XML.Cache.make()
def parse_props(text: String): Properties.T =
- try { xml_cache.props(XML.Decode.properties(YXML.parse_body(text))) }
+ try { cache.props(XML.Decode.properties(YXML.parse_body(text))) }
catch { case _: XML.Error => log_file.err("malformed properties") }
def filter_props(marker: Protocol_Message.Marker): List[Properties.T] =
@@ -850,15 +850,10 @@
/* database access */
- 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)
+ def store(options: Options, cache: XML.Cache = XML.Cache.make()): Store =
+ new Store(options, cache)
- class Store private[Build_Log](
- options: Options,
- val xml_cache: XML.Cache,
- val xz_cache: XZ.Cache)
+ class Store private[Build_Log](options: Options, val cache: XML.Cache)
{
def open_database(
user: String = options.string("build_log_database_user"),
@@ -996,7 +991,7 @@
stmt.double(13) = session.ml_timing.factor
stmt.long(14) = session.heap_size
stmt.string(15) = session.status.map(_.toString)
- stmt.bytes(16) = compress_errors(session.errors, cache = xz_cache)
+ stmt.bytes(16) = compress_errors(session.errors, cache = cache.xz)
stmt.string(17) = session.sources
stmt.execute()
}
@@ -1034,7 +1029,7 @@
{
val ml_stats: List[(String, Option[Bytes])] =
Par_List.map[(String, Session_Entry), (String, Option[Bytes])](
- { case (a, b) => (a, Properties.compress(b.ml_statistics, cache = xz_cache).proper) },
+ { case (a, b) => (a, Properties.compress(b.ml_statistics, cache = cache.xz).proper) },
build_info.sessions.iterator.filter(p => p._2.ml_statistics.nonEmpty).toList)
val entries = if (ml_stats.nonEmpty) ml_stats else List("" -> None)
for ((session_name, ml_statistics) <- entries) {
@@ -1163,11 +1158,10 @@
sources = res.get_string(Data.sources),
heap_size = res.get_long(Data.heap_size),
status = res.get_string(Data.status).map(Session_Status.withName),
- errors = uncompress_errors(res.bytes(Data.errors), cache = xz_cache),
+ errors = uncompress_errors(res.bytes(Data.errors), cache = cache.xz),
ml_statistics =
if (ml_statistics) {
- Properties.uncompress(
- res.bytes(Data.ml_statistics), cache = xz_cache, xml_cache = xml_cache)
+ Properties.uncompress(res.bytes(Data.ml_statistics), cache = cache)
}
else Nil)
session_name -> session_entry
--- a/src/Pure/Admin/build_status.scala Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/Admin/build_status.scala Sat Jan 02 22:22:34 2021 +0100
@@ -286,8 +286,7 @@
val ml_stats =
ML_Statistics(
if (ml_statistics) {
- Properties.uncompress(
- res.bytes(Build_Log.Data.ml_statistics), cache = store.xz_cache)
+ Properties.uncompress(res.bytes(Build_Log.Data.ml_statistics), cache = store.cache)
}
else Nil,
domain = ml_statistics_domain,
@@ -320,8 +319,8 @@
stored_heap = ML_Statistics.mem_scale(res.long(Build_Log.Data.heap_size)),
status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)),
errors =
- Build_Log.uncompress_errors(res.bytes(Build_Log.Data.errors),
- cache = store.xz_cache))
+ Build_Log.uncompress_errors(
+ res.bytes(Build_Log.Data.errors), cache = store.cache.xz))
val sessions = data_entries.getOrElse(data_name, Map.empty)
val session =
--- a/src/Pure/General/cache.scala Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/General/cache.scala Sat Jan 02 22:22:34 2021 +0100
@@ -16,7 +16,9 @@
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 =
+ 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)
--- a/src/Pure/General/properties.scala Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/General/properties.scala Sat Jan 02 22:22:34 2021 +0100
@@ -37,8 +37,8 @@
def encode(ps: T): Bytes = Bytes(YXML.string_of_body(XML.Encode.properties(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 decode(bs: Bytes, cache: XML.Cache = XML.Cache.none): T =
+ cache.props(XML.Decode.properties(YXML.parse_body(bs.text)))
def compress(ps: List[T],
options: XZ.Options = XZ.options(),
@@ -51,15 +51,14 @@
}
}
- def uncompress(bs: Bytes,
- cache: XZ.Cache = XZ.Cache(),
- xml_cache: XML.Cache = XML.Cache.none): List[T] =
+ def uncompress(bs: Bytes, 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))
- if (xml_cache.no_cache) ps else ps.map(xml_cache.props)
+ XML.Decode.list(XML.Decode.properties)(
+ YXML.parse_body(bs.uncompress(cache = cache.xz).text))
+ if (cache.no_cache) ps else ps.map(cache.props)
}
}
--- a/src/Pure/ML/ml_statistics.scala Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/ML/ml_statistics.scala Sat Jan 02 22:22:34 2021 +0100
@@ -99,7 +99,7 @@
private def consume(props: Properties.T): Unit = synchronized
{
if (session != null) {
- val props1 = (session.xml_cache.props(props ::: Java_Statistics.jvm_statistics()))
+ val props1 = (session.cache.props(props ::: Java_Statistics.jvm_statistics()))
session.runtime_statistics.post(Session.Runtime_Statistics(props1))
}
}
--- a/src/Pure/PIDE/command.scala Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/PIDE/command.scala Sat Jan 02 22:22:34 2021 +0100
@@ -290,7 +290,7 @@
other_id: (Document.Node.Name, Document_ID.Generic) =>
Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)],
message: XML.Elem,
- xml_cache: XML.Cache): State =
+ cache: XML.Cache): State =
message match {
case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
if (command.span.is_theory) this
@@ -329,7 +329,7 @@
target_chunk.incorporate(symbol_range) match {
case Some(range) =>
val props = atts.filterNot(Markup.position_property)
- val elem = xml_cache.elem(XML.Elem(Markup(name, props), args))
+ val elem = cache.elem(XML.Elem(Markup(name, props), args))
state.add_markup(false, target_name, Text.Info(range, elem))
case None => bad(); state
}
@@ -348,9 +348,9 @@
props match {
case Markup.Serial(i) =>
val markup_message =
- xml_cache.elem(XML.Elem(Markup(Markup.message(name), props), body))
+ cache.elem(XML.Elem(Markup(Markup.message(name), props), body))
val message_markup =
- xml_cache.elem(XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL))))
+ cache.elem(XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL))))
var st = add_result(i -> markup_message)
if (Protocol.is_inlined(message)) {
--- a/src/Pure/PIDE/document.scala Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/PIDE/document.scala Sat Jan 02 22:22:34 2021 +0100
@@ -931,12 +931,12 @@
(commands_redirection /: st.markups.redirection_iterator)({ case (graph, id) =>
graph.default_node(id, ()).default_node(st.command.id, ()).add_edge(id, st.command.id) })
- def accumulate(id: Document_ID.Generic, message: XML.Elem, xml_cache: XML.Cache)
+ def accumulate(id: Document_ID.Generic, message: XML.Elem, cache: XML.Cache)
: (Command.State, State) =
{
def update(st: Command.State): (Command.State, State) =
{
- val st1 = st.accumulate(self_id(st), other_id, message, xml_cache)
+ val st1 = st.accumulate(self_id(st), other_id, message, cache)
(st1, copy(commands_redirection = redirection(st1)))
}
execs.get(id).map(update) match {
--- a/src/Pure/PIDE/prover.scala Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/PIDE/prover.scala Sat Jan 02 22:22:34 2021 +0100
@@ -64,7 +64,7 @@
class Prover(
receiver: Prover.Receiver,
- xml_cache: XML.Cache,
+ cache: XML.Cache,
channel: System_Channel,
process: Bash.Process) extends Protocol
{
@@ -77,14 +77,14 @@
private def protocol_output(props: Properties.T, bytes: Bytes)
{
- receiver(new Prover.Protocol_Output(xml_cache.props(props), bytes))
+ receiver(new Prover.Protocol_Output(cache.props(props), bytes))
}
private def output(kind: String, props: Properties.T, body: XML.Body)
{
val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body))
val reports = Protocol_Message.reports(props, body)
- for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg)))
+ for (msg <- main :: reports) receiver(new Prover.Output(cache.elem(msg)))
}
private def exit_message(result: Process_Result)
--- a/src/Pure/PIDE/session.scala Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/PIDE/session.scala Sat Jan 02 22:22:34 2021 +0100
@@ -127,8 +127,7 @@
{
session =>
- val xml_cache: XML.Cache = XML.Cache.make()
- val xz_cache: XZ.Cache = XZ.Cache.make()
+ val cache: XML.Cache = XML.Cache.make()
def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info =
Command.Blobs_Info.none
@@ -496,7 +495,7 @@
case Protocol.Command_Timing(props, state_id, timing) if prover.defined =>
command_timings.post(Session.Command_Timing(props))
val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
- change_command(_.accumulate(state_id, xml_cache.elem(message), xml_cache))
+ change_command(_.accumulate(state_id, cache.elem(message), cache))
case Markup.Theory_Timing(props) =>
theory_timings.post(Session.Theory_Timing(props))
@@ -507,7 +506,7 @@
case Protocol.Export(args)
if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
val id = Value.Long.unapply(args.id.get).get
- val export = Export.make_entry("", args, msg.bytes, cache = xz_cache)
+ val export = Export.make_entry("", args, msg.bytes, cache)
change_command(_.add_export(id, (args.serial, export)))
case Protocol.Loading_Theory(node_name, id) =>
@@ -519,7 +518,7 @@
msg.text match {
case Protocol.Commands_Accepted(ids) =>
ids.foreach(id =>
- change_command(_.accumulate(id, Protocol.Commands_Accepted.message, xml_cache)))
+ change_command(_.accumulate(id, Protocol.Commands_Accepted.message, cache)))
case _ => bad_output()
}
@@ -554,7 +553,7 @@
case _ =>
output.properties match {
case Position.Id(state_id) =>
- change_command(_.accumulate(state_id, output.message, xml_cache))
+ change_command(_.accumulate(state_id, output.message, cache))
case _ if output.is_init =>
val init_ok =
--- a/src/Pure/PIDE/xml.scala Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/PIDE/xml.scala Sat Jan 02 22:22:34 2021 +0100
@@ -174,14 +174,15 @@
object Cache
{
def make(
- max_string: Int = isabelle.Cache.default_max_string,
+ xz: XZ.Cache = XZ.Cache.make(),
+ max_string: Int = isabelle.Cache.default_max_string,
initial_size: Int = isabelle.Cache.default_initial_size): Cache =
- new Cache(max_string, initial_size)
+ new Cache(xz, max_string, initial_size)
- val none: Cache = make(max_string = 0)
+ val none: Cache = make(XZ.Cache.none, max_string = 0)
}
- class Cache private[XML](max_string: Int, initial_size: Int)
+ class Cache private[XML](val xz: XZ.Cache, max_string: Int, initial_size: Int)
extends isabelle.Cache(max_string, initial_size)
{
protected def cache_props(x: Properties.T): Properties.T =
--- a/src/Pure/System/isabelle_process.scala Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/System/isabelle_process.scala Sat Jan 02 22:22:34 2021 +0100
@@ -62,7 +62,7 @@
case _ =>
}
- session.start(receiver => new Prover(receiver, session.xml_cache, channel, process))
+ session.start(receiver => new Prover(receiver, session.cache, channel, process))
def await_startup(): Isabelle_Process =
startup.join match {
--- a/src/Pure/Thy/export.scala Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/Thy/export.scala Sat Jan 02 22:22:34 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.Cache.none)
+ Entry("", theory_name, name, false, Future.value(false, Bytes.empty), XML.Cache.none)
sealed case class Entry(
session_name: String,
@@ -93,7 +93,7 @@
name: String,
executable: Boolean,
body: Future[(Boolean, Bytes)],
- cache: XZ.Cache)
+ cache: XML.Cache)
{
override def toString: String = name
@@ -110,7 +110,7 @@
def uncompressed: Bytes =
{
val (compressed, bytes) = body.join
- if (compressed) bytes.uncompress(cache = cache) else bytes
+ if (compressed) bytes.uncompress(cache = cache.xz) else bytes
}
def uncompressed_yxml: XML.Body =
@@ -158,17 +158,15 @@
}
def make_entry(
- session_name: String, args: Protocol.Export.Args, bytes: Bytes,
- cache: XZ.Cache): Entry =
+ session_name: String, args: Protocol.Export.Args, bytes: Bytes, cache: XML.Cache): Entry =
{
val body =
- if (args.compress) Future.fork(bytes.maybe_compress(cache = cache))
+ if (args.compress) Future.fork(bytes.maybe_compress(cache = cache.xz))
else Future.value((false, bytes))
Entry(session_name, args.theory_name, args.name, args.executable, body, cache)
}
- def read_entry(
- db: SQL.Database, cache: XZ.Cache,
+ def read_entry(db: SQL.Database, cache: XML.Cache,
session_name: String, theory_name: String, name: String): Option[Entry] =
{
val select =
@@ -188,8 +186,7 @@
})
}
- def read_entry(
- dir: Path, cache: XZ.Cache,
+ def read_entry(dir: Path, cache: XML.Cache,
session_name: String, theory_name: String, name: String): Option[Entry] =
{
val path = dir + Path.basic(theory_name) + Path.explode(name)
@@ -205,9 +202,9 @@
/* database consumer thread */
- def consumer(db: SQL.Database, cache: XZ.Cache): Consumer = new Consumer(db, cache)
+ def consumer(db: SQL.Database, cache: XML.Cache): Consumer = new Consumer(db, cache)
- class Consumer private[Export](db: SQL.Database, cache: XZ.Cache)
+ class Consumer private[Export](db: SQL.Database, cache: XML.Cache)
{
private val errors = Synchronized[List[String]](Nil)
@@ -271,9 +268,9 @@
override def toString: String = context.toString
}
- def database(
- db: SQL.Database, cache: XZ.Cache,
- session_name: String, theory_name: String): Provider =
+ def database(db: SQL.Database, cache: XML.Cache, session_name: String, theory_name: String)
+ : Provider =
+ {
new Provider {
def apply(export_name: String): Option[Entry] =
read_entry(db, cache, session_name, theory_name, export_name)
@@ -284,6 +281,7 @@
override def toString: String = db.toString
}
+ }
def snapshot(snapshot: Document.Snapshot): Provider =
new Provider {
@@ -302,9 +300,9 @@
override def toString: String = snapshot.toString
}
- def directory(
- dir: Path, cache: XZ.Cache,
- session_name: String, theory_name: String): Provider =
+ def directory(dir: Path, cache: XML.Cache, session_name: String, theory_name: String)
+ : Provider =
+ {
new Provider {
def apply(export_name: String): Option[Entry] =
read_entry(dir, cache, session_name, theory_name, export_name)
@@ -315,6 +313,7 @@
override def toString: String = dir.toString
}
+ }
}
trait Provider
@@ -364,7 +363,7 @@
for {
(theory_name, group) <- exports.toList.groupBy(_._1).toList.sortBy(_._1)
name <- group.map(_._2).sorted
- entry <- read_entry(db, store.xz_cache, session_name, theory_name, name)
+ entry <- read_entry(db, store.cache, session_name, theory_name, name)
} {
val elems = theory_name :: space_explode('/', name)
val path =
--- a/src/Pure/Thy/export_theory.scala Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/Thy/export_theory.scala Sat Jan 02 22:22:34 2021 +0100
@@ -41,8 +41,8 @@
for (theory <- Export.read_theory_names(db, session))
yield {
progress.echo("Reading theory " + theory)
- read_theory(Export.Provider.database(db, store.xz_cache, session, theory),
- session, theory, cache = cache)
+ val provider = Export.Provider.database(db, store.cache, session, theory)
+ read_theory(provider, session, theory, cache = cache)
}
}
}))
@@ -145,8 +145,8 @@
using(store.open_database(session_name))(db =>
{
db.transaction {
- read(Export.Provider.database(
- db, store.xz_cache, session_name, theory_name), session_name, theory_name)
+ val provider = Export.Provider.database(db, store.cache, session_name, theory_name)
+ read(provider, session_name, theory_name)
}
})
}
--- a/src/Pure/Thy/sessions.scala Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/Thy/sessions.scala Sat Jan 02 22:22:34 2021 +0100
@@ -1203,8 +1203,7 @@
val store: Sessions.Store,
database_server: Option[SQL.Database]) extends AutoCloseable
{
- def xml_cache: XML.Cache = store.xml_cache
- def xz_cache: XZ.Cache = store.xz_cache
+ def cache: XML.Cache = store.cache
def close { database_server.foreach(_.close) }
@@ -1231,12 +1230,12 @@
database_server match {
case Some(db) =>
sessions.view.map(session_name =>
- Export.read_entry(db, store.xz_cache, session_name, theory_name, name))
+ Export.read_entry(db, store.cache, session_name, theory_name, name))
case None =>
sessions.view.map(session_name =>
store.try_open_database(session_name) match {
case Some(db) =>
- using(db)(Export.read_entry(_, store.xz_cache, session_name, theory_name, name))
+ using(db)(Export.read_entry(_, store.cache, session_name, theory_name, name))
case None => None
})
}
@@ -1259,15 +1258,10 @@
}
}
- 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)
+ def store(options: Options, cache: XML.Cache = XML.Cache.make()): Store =
+ new Store(options, cache)
- class Store private[Sessions](
- val options: Options,
- val xml_cache: XML.Cache,
- val xz_cache: XZ.Cache)
+ class Store private[Sessions](val options: Options, val cache: XML.Cache)
{
store =>
@@ -1407,8 +1401,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 = xml_cache)
+ Properties.uncompress(read_bytes(db, name, column), cache = cache)
/* session info */
@@ -1459,11 +1452,11 @@
{
stmt.string(1) = name
stmt.bytes(2) = Properties.encode(build_log.session_timing)
- stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = xz_cache)
- stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = xz_cache)
- stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = xz_cache)
- stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = xz_cache)
- stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = xz_cache)
+ stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = cache.xz)
+ stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = cache.xz)
+ stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = cache.xz)
+ stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = cache.xz)
+ stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = cache.xz)
stmt.string(8) = build.sources
stmt.string(9) = cat_lines(build.input_heaps)
stmt.string(10) = build.output_heap getOrElse ""
@@ -1474,7 +1467,7 @@
}
def read_session_timing(db: SQL.Database, name: String): Properties.T =
- Properties.decode(read_bytes(db, name, Session_Info.session_timing), xml_cache = xml_cache)
+ Properties.decode(read_bytes(db, name, Session_Info.session_timing), cache = cache)
def read_command_timings(db: SQL.Database, name: String): List[Properties.T] =
read_properties(db, name, Session_Info.command_timings)
@@ -1492,7 +1485,7 @@
read_theory_timings(db, name).flatMap(Markup.Name.unapply)
def read_errors(db: SQL.Database, name: String): List[String] =
- Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors), cache = xz_cache)
+ Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors), cache = cache.xz)
def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
{
--- a/src/Pure/Tools/build_job.scala Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/Tools/build_job.scala Sat Jan 02 22:22:34 2021 +0100
@@ -25,7 +25,7 @@
db_context.get_export(List(session), theory, name)
def read_xml(name: String): XML.Body =
- db_context.xml_cache.body(YXML.parse_body(
+ db_context.cache.body(YXML.parse_body(
Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).uncompressed))))
(read(Export.DOCUMENT_ID).text, split_lines(read(Export.FILES).text)) match {
@@ -234,8 +234,7 @@
val resources = new Resources(sessions_structure, base, command_timings = command_timings0)
val session =
new Session(options, resources) {
- override val xml_cache: XML.Cache = store.xml_cache
- override val xz_cache: XZ.Cache = store.xz_cache
+ override val cache: XML.Cache = store.cache
override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info =
{
@@ -262,7 +261,7 @@
}
val export_consumer =
- Export.consumer(store.open_database(session_name, output = true), store.xz_cache)
+ Export.consumer(store.open_database(session_name, output = true), store.cache)
val stdout = new StringBuilder(1000)
val stderr = new StringBuilder(1000)
--- a/src/Pure/Tools/debugger.scala Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/Tools/debugger.scala Sat Jan 02 22:22:34 2021 +0100
@@ -133,7 +133,7 @@
Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes)) match {
case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
val message = XML.Elem(Markup(Markup.message(name), props), body)
- debugger.add_output(thread_name, i -> session.xml_cache.elem(message))
+ debugger.add_output(thread_name, i -> session.cache.elem(message))
true
case _ => false
}
--- a/src/Pure/term.scala Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/term.scala Sat Jan 02 22:22:34 2021 +0100
@@ -144,7 +144,7 @@
}
class Cache private[Term](max_string: Int, initial_size: Int)
- extends isabelle.Cache(max_string = max_string, initial_size = initial_size)
+ extends isabelle.Cache(max_string, initial_size)
{
protected def cache_indexname(x: Indexname): Indexname =
lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index))