Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned signature;
authorwenzelm
Thu, 06 Oct 2016 11:27:03 +0200
changeset 64063 2c5039363ea3
parent 64062 a7352cbde7d7
child 64064 f3ac9153bc0d
tuned signature;
src/Pure/Tools/build_log.scala file | annotate | diff | comparison | revisions
src/Pure/library.scala file | annotate | diff | comparison | revisions 
--- a/src/Pure/Tools/build_log.scala	Thu Oct 06 11:13:12 2016 +0200
+++ b/src/Pure/Tools/build_log.scala	Thu Oct 06 11:27:03 2016 +0200
@@ -24,7 +24,7 @@
       new Log_File(name, lines)
 
     def apply(name: String, text: String): Log_File =
-      Log_File(name, split_lines(Library.trim_line(text)).map(Library.trim_line(_)))
+      Log_File(name, Library.trim_split_lines(text))
   }
 
   class Log_File private(val name: String, val lines: List[String])
--- a/src/Pure/library.scala	Thu Oct 06 11:13:12 2016 +0200
+++ b/src/Pure/library.scala	Thu Oct 06 11:27:03 2016 +0200
@@ -130,6 +130,9 @@
     else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1)
     else s
 
+  def trim_split_lines(s: String): List[String] =
+    split_lines(trim_line(s)).map(trim_line(_))
+
 
   /* quote */
isabelle