# HG changeset patch
# User wenzelm
# Date 1495474441 -7200
# Node ID 692e428803c8ff69ed448cd68be118bde687396c
# Parent  c28143ae38cd50c8e20075c6d0893d91ba39e19d
clarified signature;

diff -r c28143ae38cd -r 692e428803c8 src/Pure/PIDE/line.scala
--- a/src/Pure/PIDE/line.scala	Mon May 22 15:19:44 2017 +0200
+++ b/src/Pure/PIDE/line.scala	Mon May 22 19:34:01 2017 +0200
@@ -95,7 +95,7 @@
   object Document
   {
     def apply(text: String): Document =
-      Document(logical_lines(text).map(s => Line(Library.trim_substring(s))))
+      Document(logical_lines(text).map(s => Line(Library.isolate_substring(s))))
 
     val empty: Document = apply("")
 
diff -r c28143ae38cd -r 692e428803c8 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Mon May 22 15:19:44 2017 +0200
+++ b/src/Pure/PIDE/xml.scala	Mon May 22 19:34:01 2017 +0200
@@ -161,7 +161,7 @@
         lookup(x) match {
           case Some(y) => y
           case None =>
-            val z = Library.trim_substring(x)
+            val z = Library.isolate_substring(x)
             if (z.length > max_string) z else store(z)
         }
     private def cache_props(x: Properties.T): Properties.T =
@@ -169,7 +169,7 @@
       else
         lookup(x) match {
           case Some(y) => y
-          case None => store(x.map(p => (Library.trim_substring(p._1).intern, cache_string(p._2))))
+          case None => store(x.map(p => (Library.isolate_substring(p._1).intern, cache_string(p._2))))
         }
     private def cache_markup(x: Markup): Markup =
       lookup(x) match {
diff -r c28143ae38cd -r 692e428803c8 src/Pure/library.scala
--- a/src/Pure/library.scala	Mon May 22 15:19:44 2017 +0200
+++ b/src/Pure/library.scala	Mon May 22 19:34:01 2017 +0200
@@ -142,7 +142,7 @@
   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)
+  def isolate_substring(s: String): String = new String(s.toCharArray)
 
 
   /* quote */