--- a/src/Pure/General/properties.scala Fri May 26 11:11:25 2017 +0200
+++ b/src/Pure/General/properties.scala Fri May 26 11:33:09 2017 +0200
@@ -67,13 +67,8 @@
/* multi-line entries */
- val separator = '\u000b'
-
- def encode_lines(s: java.lang.String): java.lang.String = s.replace('\n', separator)
- def decode_lines(s: java.lang.String): java.lang.String = s.replace(separator, '\n')
-
- def encode_lines(props: T): T = props.map({ case (a, b) => (a, encode_lines(b)) })
- def decode_lines(props: T): T = props.map({ case (a, b) => (a, decode_lines(b)) })
+ def encode_lines(props: T): T = props.map({ case (a, b) => (a, Library.encode_lines(b)) })
+ def decode_lines(props: T): T = props.map({ case (a, b) => (a, Library.decode_lines(b)) })
def lines_nonempty(x: java.lang.String, ys: List[java.lang.String]): Properties.T =
if (ys.isEmpty) Nil else List((x, cat_lines(ys)))
--- a/src/Pure/library.scala Fri May 26 11:11:25 2017 +0200
+++ b/src/Pure/library.scala Fri May 26 11:33:09 2017 +0200
@@ -115,6 +115,9 @@
else ""
}
+ def encode_lines(s: String): String = s.replace('\n', '\u000b')
+ def decode_lines(s: String): String = s.replace('\u000b', '\n')
+
/* strings */