# HG changeset patch # User wenzelm # Date 1397641946 -7200 # Node ID 628e039cc34d9c9b2ff1ea71e7d7376f097d58d2 # Parent c4424d8c890fe70b356c8b5a739526835844c421 more specific support for sequence of words; diff -r c4424d8c890f -r 628e039cc34d src/Pure/General/completion.scala --- 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) diff -r c4424d8c890f -r 628e039cc34d src/Pure/General/word.scala --- 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) } diff -r c4424d8c890f -r 628e039cc34d src/Pure/PIDE/yxml.scala --- 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)) diff -r c4424d8c890f -r 628e039cc34d src/Pure/System/options.scala --- 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 diff -r c4424d8c890f -r 628e039cc34d src/Pure/library.scala --- 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 "" } diff -r c4424d8c890f -r 628e039cc34d src/Tools/jEdit/src/rendering.scala --- 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 = diff -r c4424d8c890f -r 628e039cc34d src/Tools/jEdit/src/symbols_dockable.scala --- 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) }