more operations;
authorwenzelm
Fri Oct 07 14:17:20 2016 +0200 (2016-10-07)
changeset 64083fef1a0a59c12
parent 64082 d57c7295f601
child 64084 bca58a11efde
more operations;
src/Pure/Tools/build_log.scala
     1.1 --- a/src/Pure/Tools/build_log.scala	Fri Oct 07 13:58:10 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 14:17:20 2016 +0200
     1.3 @@ -51,6 +51,16 @@
     1.4  
     1.5    object Log_File
     1.6    {
     1.7 +    def apply(path: Path): Log_File =
     1.8 +    {
     1.9 +      val (path_name, ext) = path.expand.split_ext
    1.10 +      val text =
    1.11 +        if (ext == "gz") File.read_gzip(path)
    1.12 +        else if (ext == "xz") File.read_xz(path)
    1.13 +        else File.read(path)
    1.14 +      apply(path_name.base.implode, text)
    1.15 +    }
    1.16 +
    1.17      def apply(name: String, lines: List[String]): Log_File =
    1.18        new Log_File(name, lines)
    1.19