# HG changeset patch
# User wenzelm
# Date 1475858514 -7200
# Node ID 5a68280112b3f42cfd6daff4fcc47f1436d37537
# Parent  10d719dbb3ee4d45fa6da254572ac63891628b4c
more operations;

diff -r 10d719dbb3ee -r 5a68280112b3 src/Pure/Tools/build_log.scala
--- a/src/Pure/Tools/build_log.scala	Fri Oct 07 18:30:56 2016 +0200
+++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 18:41:54 2016 +0200
@@ -7,6 +7,7 @@
 package isabelle
 
 
+import java.io.{File => JFile}
 import java.time.ZonedDateTime
 import java.time.format.{DateTimeFormatter, DateTimeParseException}
 
@@ -51,21 +52,28 @@
 
   object Log_File
   {
-    def apply(path: Path): Log_File =
-    {
-      val (path_name, ext) = path.expand.split_ext
-      val text =
-        if (ext == "gz") File.read_gzip(path)
-        else if (ext == "xz") File.read_xz(path)
-        else File.read(path)
-      apply(path_name.base.implode, text)
-    }
-
     def apply(name: String, lines: List[String]): Log_File =
       new Log_File(name, lines)
 
     def apply(name: String, text: String): Log_File =
       Log_File(name, Library.trim_split_lines(text))
+
+    def apply(file: JFile): Log_File =
+    {
+      val name = file.getName
+      val (base_name, text) =
+        Library.try_unsuffix(".gz", name) match {
+          case Some(base_name) => (base_name, File.read_gzip(file))
+          case None =>
+            Library.try_unsuffix(".xz", name) match {
+              case Some(base_name) => (base_name, File.read_xz(file))
+              case None => (name, File.read(file))
+            }
+          }
+      apply(base_name, text)
+    }
+
+    def apply(path: Path): Log_File = apply(path.file)
   }
 
   class Log_File private(val name: String, val lines: List[String])