more operations;
authorwenzelm
Fri Oct 07 18:41:54 2016 +0200 (2016-10-07)
changeset 640905a68280112b3
parent 64089 10d719dbb3ee
child 64091 f8dfba90e73f
more operations;
src/Pure/Tools/build_log.scala
     1.1 --- a/src/Pure/Tools/build_log.scala	Fri Oct 07 18:30:56 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 18:41:54 2016 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 +import java.io.{File => JFile}
     1.8  import java.time.ZonedDateTime
     1.9  import java.time.format.{DateTimeFormatter, DateTimeParseException}
    1.10  
    1.11 @@ -51,21 +52,28 @@
    1.12  
    1.13    object Log_File
    1.14    {
    1.15 -    def apply(path: Path): Log_File =
    1.16 -    {
    1.17 -      val (path_name, ext) = path.expand.split_ext
    1.18 -      val text =
    1.19 -        if (ext == "gz") File.read_gzip(path)
    1.20 -        else if (ext == "xz") File.read_xz(path)
    1.21 -        else File.read(path)
    1.22 -      apply(path_name.base.implode, text)
    1.23 -    }
    1.24 -
    1.25      def apply(name: String, lines: List[String]): Log_File =
    1.26        new Log_File(name, lines)
    1.27  
    1.28      def apply(name: String, text: String): Log_File =
    1.29        Log_File(name, Library.trim_split_lines(text))
    1.30 +
    1.31 +    def apply(file: JFile): Log_File =
    1.32 +    {
    1.33 +      val name = file.getName
    1.34 +      val (base_name, text) =
    1.35 +        Library.try_unsuffix(".gz", name) match {
    1.36 +          case Some(base_name) => (base_name, File.read_gzip(file))
    1.37 +          case None =>
    1.38 +            Library.try_unsuffix(".xz", name) match {
    1.39 +              case Some(base_name) => (base_name, File.read_xz(file))
    1.40 +              case None => (name, File.read(file))
    1.41 +            }
    1.42 +          }
    1.43 +      apply(base_name, text)
    1.44 +    }
    1.45 +
    1.46 +    def apply(path: Path): Log_File = apply(path.file)
    1.47    }
    1.48  
    1.49    class Log_File private(val name: String, val lines: List[String])