src/Pure/PIDE/xml.scala

       else if (Library.is_small_int(x)) Library.signed_string_of_int(Integer.parseInt(x))
       else
         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 =
       if (x.isEmpty) x
       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 {
         case Some(y) => y
         case None =>