# HG changeset patch
# User wenzelm
# Date 1483802201 -3600
# Node ID 00488a8c042f668c8e9b9563bd6b976e94ac8bbb
# Parent  bebe7a164068c11949a5de09a909b17f64712575
Line.Document consists of independently allocated strings;
tuned signature;

diff -r bebe7a164068 -r 00488a8c042f src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Sat Jan 07 15:25:01 2017 +0100
+++ b/src/Pure/PIDE/line.scala	Sat Jan 07 16:16:41 2017 +0100
@@ -90,7 +90,7 @@
   object Document
   {
     def apply(text: String, text_length: Text.Length): Document =
-      Document(logical_lines(text).map(Line(_)), text_length)
+      Document(logical_lines(text).map(s => Line(Library.trim_substring(s))), text_length)
   }
 
   sealed case class Document(lines: List[Line], text_length: Text.Length)
diff -r bebe7a164068 -r 00488a8c042f src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Sat Jan 07 15:25:01 2017 +0100
+++ b/src/Pure/PIDE/xml.scala	Sat Jan 07 16:16:41 2017 +0100
@@ -148,8 +148,6 @@
       x
     }
 
-    private def trim_bytes(s: String): String = new String(s.toCharArray)
-
     private def cache_string(x: String): String =
       if (x == "true") "true"
       else if (x == "false") "false"
@@ -159,7 +157,7 @@
         lookup(x) match {
           case Some(y) => y
           case None =>
-            val z = trim_bytes(x)
+            val z = Library.trim_substring(x)
             if (z.length > max_string) z else store(z)
         }
     private def cache_props(x: Properties.T): Properties.T =
@@ -167,7 +165,7 @@
       else
         lookup(x) match {
           case Some(y) => y
-          case None => store(x.map(p => (trim_bytes(p._1).intern, cache_string(p._2))))
+          case None => store(x.map(p => (Library.trim_substring(p._1).intern, cache_string(p._2))))
         }
     private def cache_markup(x: Markup): Markup =
       lookup(x) match {
diff -r bebe7a164068 -r 00488a8c042f src/Pure/library.scala
--- a/src/Pure/library.scala	Sat Jan 07 15:25:01 2017 +0100
+++ b/src/Pure/library.scala	Sat Jan 07 16:16:41 2017 +0100
@@ -139,6 +139,8 @@
   def trim_split_lines(s: String): List[String] =
     split_lines(trim_line(s)).map(trim_line(_))
 
+  def trim_substring(s: String): String = new String(s.toCharArray)
+
 
   /* quote */