# HG changeset patch
# User wenzelm
# Date 1700323094 -3600
# Node ID 24e686fe043ed9e9d25e54a49e3f0bfb9b245f1e
# Parent  417b490c9b89ab01ee832f3d947f02a7c10f9fd5
clarified Log_File.cache: reuse existing Store.cache / Build_Log.Store.cache;

diff -r 417b490c9b89 -r 24e686fe043e src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Nov 18 15:44:46 2023 +0100
+++ b/src/Pure/Admin/build_history.scala	Sat Nov 18 16:58:14 2023 +0100
@@ -257,15 +257,15 @@
 
       val build_end = Date.now()
 
+      val store = Store(options + "build_database_server=false")
+
       val build_info: Build_Log.Build_Info =
-        Build_Log.Log_File(log_path.file_name, build_result.out_lines).
+        Build_Log.Log_File(log_path.file_name, build_result.out_lines, cache = store.cache).
           parse_build_info(ml_statistics = true)
 
 
       /* output log */
 
-      val store = Store(options + "build_database_server=false")
-
       val meta_info =
         Properties.lines_nonempty(Build_Log.Prop.build_tags.name, build_tags) :::
         Properties.lines_nonempty(Build_Log.Prop.build_args.name, build_args1) :::
@@ -317,7 +317,7 @@
               using(SQLite.open_database(database))(store.read_ml_statistics(_, session_name))
             }
             else if (log_gz.is_file) {
-              Build_Log.Log_File.read(log_gz.file)
+              Build_Log.Log_File.read(log_gz.file, cache = store.cache)
                 .parse_session_info(ml_statistics = true).ml_statistics
             }
             else Nil
diff -r 417b490c9b89 -r 24e686fe043e src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sat Nov 18 15:44:46 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Sat Nov 18 16:58:14 2023 +0100
@@ -102,19 +102,16 @@
     }
     def plain_name(file: JFile): String = plain_name(file.getName)
 
-    def apply(name: String, lines: List[String]): Log_File =
-      new Log_File(plain_name(name), lines.map(Library.trim_line))
+    def apply(name: String, lines: List[String], cache: XML.Cache = XML.Cache.none): Log_File =
+      new Log_File(plain_name(name), lines.map(s => cache.string(Library.trim_line(s))), cache)
 
-    def apply(name: String, text: String): Log_File =
-      new Log_File(plain_name(name), Library.trim_split_lines(text))
-
-    def read(file: JFile, cache: Compress.Cache = Compress.Cache.none): Log_File = {
+    def read(file: JFile, cache: XML.Cache = XML.Cache.none): Log_File = {
       val name = file.getName
       val text =
         if (File.is_gz(name)) File.read_gzip(file)
-        else if (File.is_xz(name)) Bytes.read(file).uncompress_xz(cache = cache).text
+        else if (File.is_xz(name)) Bytes.read(file).uncompress_xz(cache = cache.compress).text
         else File.read(file)
-      apply(name, text)
+      apply(name, Library.trim_split_lines(text), cache = cache)
     }
 
 
@@ -186,7 +183,11 @@
     }
   }
 
-  class Log_File private(val name: String, val lines: List[String]) {
+  class Log_File private(
+    val name: String,
+    val lines: List[String],
+    val cache: XML.Cache
+  ) {
     log_file =>
 
     override def toString: String = name
@@ -235,10 +236,8 @@
 
     /* properties (YXML) */
 
-    val cache: XML.Cache = XML.Cache.make()
-
     def parse_props(text: String): Properties.T =
-      try { cache.props(XML.Decode.properties(YXML.parse_body(text))) }
+      try { cache.props(XML.Decode.properties(YXML.parse_body(text, cache = cache))) }
       catch { case _: XML.Error => log_file.err("malformed properties") }
 
     def filter_props(marker: Protocol_Message.Marker): List[Properties.T] =
@@ -1093,7 +1092,7 @@
 
       try {
         for (file <- files.iterator if status.exists(_.required(file))) {
-          Exn.result { Log_File.read(file, cache = cache.compress) } match {
+          Exn.result { Log_File.read(file, cache = cache) } match {
             case Exn.Res(log_file) => consumer.send(log_file)
             case Exn.Exn(exn) => add_error(Log_File.plain_name(file), exn)
           }
diff -r 417b490c9b89 -r 24e686fe043e src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sat Nov 18 15:44:46 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Sat Nov 18 16:58:14 2023 +0100
@@ -480,7 +480,7 @@
           val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test)
 
           val build_log =
-            Build_Log.Log_File(session_name, process_result.out_lines).
+            Build_Log.Log_File(session_name, process_result.out_lines, cache = store.cache).
               parse_session_info(
                 command_timings = true,
                 theory_timings = true,