# HG changeset patch
# User wenzelm
# Date 1614617084 -3600
# Node ID 91703452523d316d9220234680f8dafcd40c4b57
# Parent  d045cdbdf243318a977db8834e9ca2a5aa5d3a0c
tuned;

diff -r d045cdbdf243 -r 91703452523d src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Mar 01 15:09:57 2021 +0100
+++ b/src/Pure/library.scala	Mon Mar 01 17:44:44 2021 +0100
@@ -112,6 +112,14 @@
     else ""
   }
 
+  def trim_line(s: String): String =
+    if (s.endsWith("\r\n")) s.substring(0, s.length - 2)
+    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)
+
   def encode_lines(s: String): String = s.replace('\n', '\u000b')
   def decode_lines(s: String): String = s.replace('\u000b', '\n')
 
@@ -134,14 +142,6 @@
   def perhaps_unprefix(prfx: String, s: String): String = try_unprefix(prfx, s) getOrElse s
   def perhaps_unsuffix(sffx: String, s: String): String = try_unsuffix(sffx, s) getOrElse s
 
-  def trim_line(s: String): String =
-    if (s.endsWith("\r\n")) s.substring(0, s.length - 2)
-    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)
-
   def isolate_substring(s: String): String = new String(s.toCharArray)
 
   def strip_ansi_color(s: String): String =