more specific support for sequence of words;

--- a/src/Pure/General/completion.scala	Wed Apr 16 09:38:40 2014 +0200
+++ b/src/Pure/General/completion.scala	Wed Apr 16 11:52:26 2014 +0200
@@ -173,7 +173,9 @@
           if xname1 != original
           (full_name, descr_name) =
             if (kind == "") (name, quote(decode(name)))
-            else (kind + "." + name, Word.plain_words(kind) + " " + quote(decode(name)))
+            else
+             (kind + "." + name,
+              Word.implode(Word.explode('_', kind)) + " " + quote(decode(name)))
           description = List(xname1, "(" + descr_name + ")")
         } yield Item(range, original, full_name, description, xname1, 0, true)
 

--- a/src/Pure/General/word.scala	Wed Apr 16 09:38:40 2014 +0200
+++ b/src/Pure/General/word.scala	Wed Apr 16 11:52:26 2014 +0200
@@ -13,6 +13,8 @@
 
 object Word
 {
+  /* case */
+
   def lowercase(str: String): String = str.toLowerCase(Locale.ROOT)
   def uppercase(str: String): String = str.toUpperCase(Locale.ROOT)
 
@@ -27,7 +29,18 @@
   def is_all_caps(str: String): Boolean =
     str.length > 0 && str.forall(Character.isUpperCase(_))
 
-  def plain_words(str: String): String =
-    space_explode('_', str).mkString(" ")
+
+  /* sequence of words */
+
+  def implode(words: Iterable[String]): String = words.iterator.mkString(" ")
+
+  def explode(sep: Char => Boolean, text: String): List[String] =
+    Library.separated_chunks(sep, text).map(_.toString).filter(_ != "").toList
+
+  def explode(sep: Char, text: String): List[String] =
+    explode(_ == sep, text)
+
+  def explode(text: String): List[String] =
+    explode(Symbol.is_ascii_blank(_), text)
 }
 

--- a/src/Pure/PIDE/yxml.scala	Wed Apr 16 09:38:40 2014 +0200
+++ b/src/Pure/PIDE/yxml.scala	Wed Apr 16 11:52:26 2014 +0200
@@ -18,6 +18,10 @@
 
   val X = '\5'
   val Y = '\6'
+
+  val is_X = (c: Char) => c == X
+  val is_Y = (c: Char) => c == Y
+
   val X_string = X.toString
   val Y_string = Y.toString
 
@@ -93,10 +97,10 @@
 
     /* parse chunks */
 
-    for (chunk <- Library.separated_chunks(X, source) if chunk.length != 0) {
+    for (chunk <- Library.separated_chunks(is_X, source) if chunk.length != 0) {
       if (chunk.length == 1 && chunk.charAt(0) == Y) pop()
       else {
-        Library.separated_chunks(Y, chunk).toList match {
+        Library.separated_chunks(is_Y, chunk).toList match {
           case ch :: name :: atts if ch.length == 0 =>
             push(name.toString, atts.map(parse_attrib))
           case txts => for (txt <- txts) add(XML.Text(txt.toString))

--- a/src/Pure/System/options.scala	Wed Apr 16 09:38:40 2014 +0200
+++ b/src/Pure/System/options.scala	Wed Apr 16 11:52:26 2014 +0200
@@ -52,13 +52,13 @@
 
     def title(strip: String = ""): String =
     {
-      val words = space_explode('_', name)
+      val words = Word.explode('_', name)
       val words1 =
         words match {
           case word :: rest if word == strip => rest
           case _ => words
         }
-      words1.map(Word.capitalize(_)).mkString(" ")
+      Word.implode(words1.map(Word.capitalize(_)))
     }
 
     def unknown: Boolean = typ == Unknown

--- a/src/Pure/library.scala	Wed Apr 16 09:38:40 2014 +0200
+++ b/src/Pure/library.scala	Wed Apr 16 11:52:26 2014 +0200
@@ -52,13 +52,13 @@
     result.toList
   }
 
-  def separated_chunks(sep: Char, source: CharSequence): Iterator[CharSequence] =
+  def separated_chunks(sep: Char => Boolean, source: CharSequence): Iterator[CharSequence] =
     new Iterator[CharSequence] {
       private val end = source.length
       private def next_chunk(i: Int): Option[(CharSequence, Int)] =
       {
         if (i < end) {
-          var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
+          var j = i; do j += 1 while (j < end && !sep(source.charAt(j)))
           Some((source.subSequence(i + 1, j), j))
         }
         else None
@@ -74,7 +74,7 @@
     }
 
   def space_explode(sep: Char, str: String): List[String] =
-    separated_chunks(sep, str).map(_.toString).toList
+    separated_chunks(_ == sep, str).map(_.toString).toList
 
 
   /* lines */
@@ -91,7 +91,7 @@
 
   def first_line(source: CharSequence): String =
   {
-    val lines = separated_chunks('\n', source)
+    val lines = separated_chunks(_ == '\n', source)
     if (lines.hasNext) lines.next.toString
     else ""
   }

--- a/src/Tools/jEdit/src/rendering.scala	Wed Apr 16 09:38:40 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Wed Apr 16 11:52:26 2014 +0200
@@ -468,7 +468,7 @@
           case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
             Some(Text.Info(r, (t1 + t2, info)))
           case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
-            val kind1 = Word.plain_words(kind)
+            val kind1 = Word.implode(Word.explode('_', kind))
             val txt1 = kind1 + " " + quote(name)
             val t = prev.info._1
             val txt2 =

--- a/src/Tools/jEdit/src/symbols_dockable.scala	Wed Apr 16 09:38:40 2014 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Wed Apr 16 11:52:26 2014 +0200
@@ -75,7 +75,7 @@
           results_panel.contents.clear
           val results =
             (searchspace filter
-              (Word.lowercase(search.text).split("\\s+") forall _._2.contains)
+              (Word.explode(Word.lowercase(search.text)) forall _._2.contains)
               take (max_results + 1)).toList
           for ((sym, _) <- results)
             results_panel.contents += new Symbol_Component(sym)
@@ -85,7 +85,7 @@
         }
       reactions += { case ValueChanged(`search`) => delay_search.invoke() }
     }, "Search Symbols")
-    pages.map(p => p.title = space_explode('_', p.title).map(Word.capitalize(_)).mkString(" "))
+    pages.map(p => p.title = Word.implode(Word.explode('_', p.title).map(Word.capitalize(_))))
   }
   set_content(group_tabs)
 }