# HG changeset patch
# User wenzelm
# Date 1698765847 -3600
# Node ID b02f8fb6b1b6eb4e69ee301ad43159e845266e08
# Parent  1bd52b048f8ed1b1887b10d4618104dc75ba7d2d
clarified signature;

diff -r 1bd52b048f8e -r b02f8fb6b1b6 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Tue Oct 31 16:15:59 2023 +0100
+++ b/src/Pure/Admin/build_history.scala	Tue Oct 31 16:24:07 2023 +0100
@@ -317,7 +317,8 @@
               using(SQLite.open_database(database))(store.read_ml_statistics(_, session_name))
             }
             else if (log_gz.is_file) {
-              Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics
+              Build_Log.Log_File.read(log_gz.file)
+                .parse_session_info(ml_statistics = true).ml_statistics
             }
             else Nil
 
diff -r 1bd52b048f8e -r b02f8fb6b1b6 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Tue Oct 31 16:15:59 2023 +0100
+++ b/src/Pure/Admin/build_log.scala	Tue Oct 31 16:24:07 2023 +0100
@@ -108,7 +108,7 @@
     def apply(name: String, text: String): Log_File =
       new Log_File(plain_name(name), Library.trim_split_lines(text))
 
-    def apply(file: JFile): Log_File = {
+    def read(file: JFile): Log_File = {
       val name = file.getName
       val text =
         if (File.is_gz(name)) File.read_gzip(file)
@@ -117,8 +117,6 @@
       apply(name, text)
     }
 
-    def apply(path: Path): Log_File = apply(path.file)
-
 
     /* log file collections */
 
@@ -1086,7 +1084,7 @@
         for (file <- files.iterator if status.exists(_.required(file))) {
           val log_name = Log_File.plain_name(file)
           progress.echo("Log " + quote(log_name), verbose = true)
-          Exn.result { Log_File(file) } match {
+          Exn.result { Log_File.read(file) } match {
             case Exn.Res(log_file) => consumer.send(log_file)
             case Exn.Exn(exn) => add_error(log_name, exn)
           }