tuned signature;
authorwenzelm
Thu Oct 06 11:27:03 2016 +0200 (2016-10-06)
changeset 640632c5039363ea3
parent 64062 a7352cbde7d7
child 64064 f3ac9153bc0d
tuned signature;
src/Pure/Tools/build_log.scala
src/Pure/library.scala
     1.1 --- a/src/Pure/Tools/build_log.scala	Thu Oct 06 11:13:12 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Thu Oct 06 11:27:03 2016 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4        new Log_File(name, lines)
     1.5  
     1.6      def apply(name: String, text: String): Log_File =
     1.7 -      Log_File(name, split_lines(Library.trim_line(text)).map(Library.trim_line(_)))
     1.8 +      Log_File(name, Library.trim_split_lines(text))
     1.9    }
    1.10  
    1.11    class Log_File private(val name: String, val lines: List[String])
     2.1 --- a/src/Pure/library.scala	Thu Oct 06 11:13:12 2016 +0200
     2.2 +++ b/src/Pure/library.scala	Thu Oct 06 11:27:03 2016 +0200
     2.3 @@ -130,6 +130,9 @@
     2.4      else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1)
     2.5      else s
     2.6  
     2.7 +  def trim_split_lines(s: String): List[String] =
     2.8 +    split_lines(trim_line(s)).map(trim_line(_))
     2.9 +
    2.10  
    2.11    /* quote */
    2.12