# HG changeset patch # User wenzelm # Date 1397633920 -7200 # Node ID c4424d8c890fe70b356c8b5a739526835844c421 # Parent 2cc2cb56cbdd0d3d299bea05483a274a619e623a tuned signature -- separate module Word; diff -r 2cc2cb56cbdd -r c4424d8c890f src/Pure/GUI/color_value.scala --- a/src/Pure/GUI/color_value.scala Tue Apr 15 22:41:10 2014 +0200 +++ b/src/Pure/GUI/color_value.scala Wed Apr 16 09:38:40 2014 +0200 @@ -31,7 +31,7 @@ val g = new java.lang.Integer(c.getGreen) val b = new java.lang.Integer(c.getBlue) val a = new java.lang.Integer(c.getAlpha) - Library.uppercase(String.format("%02x%02x%02x%02x", r, g, b, a)) + Word.uppercase(String.format("%02x%02x%02x%02x", r, g, b, a)) } def apply(s: String): Color = diff -r 2cc2cb56cbdd -r c4424d8c890f src/Pure/General/completion.scala --- a/src/Pure/General/completion.scala Tue Apr 15 22:41:10 2014 +0200 +++ b/src/Pure/General/completion.scala Wed Apr 16 09:38:40 2014 +0200 @@ -173,7 +173,7 @@ if xname1 != original (full_name, descr_name) = if (kind == "") (name, quote(decode(name))) - else (kind + "." + name, Library.plain_words(kind) + " " + quote(decode(name))) + else (kind + "." + name, Word.plain_words(kind) + " " + quote(decode(name))) description = List(xname1, "(" + descr_name + ")") } yield Item(range, original, full_name, description, xname1, 0, true) diff -r 2cc2cb56cbdd -r c4424d8c890f src/Pure/General/word.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/word.scala Wed Apr 16 09:38:40 2014 +0200 @@ -0,0 +1,33 @@ +/* Title: Pure/General/word.scala + Module: PIDE + Author: Makarius + +Support for plain text words. +*/ + +package isabelle + + +import java.util.Locale + + +object Word +{ + def lowercase(str: String): String = str.toLowerCase(Locale.ROOT) + def uppercase(str: String): String = str.toUpperCase(Locale.ROOT) + + def capitalize(str: String): String = + if (str.length == 0) str + else uppercase(str.substring(0, 1)) + str.substring(1) + + def is_capitalized(str: String): Boolean = + str.length > 0 && + Character.isUpperCase(str(0)) && str.substring(1).forall(Character.isLowerCase(_)) + + def is_all_caps(str: String): Boolean = + str.length > 0 && str.forall(Character.isUpperCase(_)) + + def plain_words(str: String): String = + space_explode('_', str).mkString(" ") +} + diff -r 2cc2cb56cbdd -r c4424d8c890f src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Tue Apr 15 22:41:10 2014 +0200 +++ b/src/Pure/System/isabelle_system.scala Wed Apr 16 09:38:40 2014 +0200 @@ -149,7 +149,7 @@ val rest = posix_path match { case Cygdrive(drive, rest) => - result_path ++= (Library.uppercase(drive) + ":" + JFile.separator) + result_path ++= (Word.uppercase(drive) + ":" + JFile.separator) rest case Named_Root(root, rest) => result_path ++= JFile.separator @@ -183,7 +183,7 @@ jvm_path.replace('/', '\\') match { case Platform_Root(rest) => "/" + rest.replace('\\', '/') case Drive(letter, rest) => - "/cygdrive/" + Library.lowercase(letter) + + "/cygdrive/" + Word.lowercase(letter) + (if (rest == "") "" else "/" + rest.replace('\\', '/')) case path => path.replace('\\', '/') } diff -r 2cc2cb56cbdd -r c4424d8c890f src/Pure/System/options.scala --- a/src/Pure/System/options.scala Tue Apr 15 22:41:10 2014 +0200 +++ b/src/Pure/System/options.scala Wed Apr 16 09:38:40 2014 +0200 @@ -21,7 +21,7 @@ sealed abstract class Type { - def print: String = Library.lowercase(toString) + def print: String = Word.lowercase(toString) } case object Bool extends Type case object Int extends Type @@ -58,7 +58,7 @@ case word :: rest if word == strip => rest case _ => words } - words1.map(Library.capitalize(_)).mkString(" ") + words1.map(Word.capitalize(_)).mkString(" ") } def unknown: Boolean = typ == Unknown diff -r 2cc2cb56cbdd -r c4424d8c890f src/Pure/build-jars --- a/src/Pure/build-jars Tue Apr 15 22:41:10 2014 +0200 +++ b/src/Pure/build-jars Wed Apr 16 09:38:40 2014 +0200 @@ -32,6 +32,7 @@ General/time.scala General/timing.scala General/url.scala + General/word.scala General/xz_file.scala GUI/color_value.scala GUI/gui.scala diff -r 2cc2cb56cbdd -r c4424d8c890f src/Pure/library.scala --- a/src/Pure/library.scala Tue Apr 15 22:41:10 2014 +0200 +++ b/src/Pure/library.scala Wed Apr 16 09:38:40 2014 +0200 @@ -10,7 +10,6 @@ import scala.collection.mutable -import java.util.Locale import java.util.concurrent.{Future => JFuture, TimeUnit} @@ -97,26 +96,9 @@ else "" } - def plain_words(str: String): String = - space_explode('_', str).mkString(" ") - /* strings */ - def lowercase(str: String): String = str.toLowerCase(Locale.ROOT) - def uppercase(str: String): String = str.toUpperCase(Locale.ROOT) - - def capitalize(str: String): String = - if (str.length == 0) str - else uppercase(str.substring(0, 1)) + str.substring(1) - - def is_capitalized(str: String): Boolean = - str.length > 0 && - Character.isUpperCase(str(0)) && str.substring(1).forall(Character.isLowerCase(_)) - - def is_all_caps(str: String): Boolean = - str.length > 0 && str.forall(Character.isUpperCase(_)) - def try_unprefix(prfx: String, s: String): Option[String] = if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None diff -r 2cc2cb56cbdd -r c4424d8c890f src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Apr 15 22:41:10 2014 +0200 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Apr 16 09:38:40 2014 +0200 @@ -201,7 +201,7 @@ for (line <- split_lines(JEdit_Lib.buffer_text(buffer)) if !stopped) { line match { case Heading1(s) => - data.root.add(make_node(Library.capitalize(s), offset, offset + line.length)) + data.root.add(make_node(Word.capitalize(s), offset, offset + line.length)) case Heading2(s) => data.root.getLastChild.asInstanceOf[DefaultMutableTreeNode] .add(make_node(s, offset, offset + line.length)) diff -r 2cc2cb56cbdd -r c4424d8c890f src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Tue Apr 15 22:41:10 2014 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Wed Apr 16 09:38:40 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 = Library.plain_words(kind) + val kind1 = Word.plain_words(kind) val txt1 = kind1 + " " + quote(name) val t = prev.info._1 val txt2 = diff -r 2cc2cb56cbdd -r c4424d8c890f src/Tools/jEdit/src/spell_checker.scala --- a/src/Tools/jEdit/src/spell_checker.scala Tue Apr 15 22:41:10 2014 +0200 +++ b/src/Tools/jEdit/src/spell_checker.scala Wed Apr 16 09:38:40 2014 +0200 @@ -248,9 +248,9 @@ def check(word: String): Boolean = contains(word) || - Library.is_all_caps(word) && contains(Library.lowercase(word)) || - Library.is_capitalized(word) && - (contains(Library.lowercase(word)) || contains(Library.uppercase(word))) + Word.is_all_caps(word) && contains(Word.lowercase(word)) || + Word.is_capitalized(word) && + (contains(Word.lowercase(word)) || contains(Word.uppercase(word))) def complete(word: String): List[String] = if (check(word)) Nil diff -r 2cc2cb56cbdd -r c4424d8c890f src/Tools/jEdit/src/symbols_dockable.scala --- a/src/Tools/jEdit/src/symbols_dockable.scala Tue Apr 15 22:41:10 2014 +0200 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Wed Apr 16 09:38:40 2014 +0200 @@ -21,7 +21,7 @@ { val searchspace = for ((group, symbols) <- Symbol.groups; sym <- symbols) - yield (sym, Library.lowercase(sym)) + yield (sym, Word.lowercase(sym)) private class Symbol_Component(val symbol: String) extends Button { @@ -75,7 +75,7 @@ results_panel.contents.clear val results = (searchspace filter - (Library.lowercase(search.text).split("\\s+") forall _._2.contains) + (Word.lowercase(search.text).split("\\s+") 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(Library.capitalize(_)).mkString(" ")) + pages.map(p => p.title = space_explode('_', p.title).map(Word.capitalize(_)).mkString(" ")) } set_content(group_tabs) } diff -r 2cc2cb56cbdd -r c4424d8c890f src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Tue Apr 15 22:41:10 2014 +0200 +++ b/src/Tools/jEdit/src/theories_dockable.scala Wed Apr 16 09:38:40 2014 +0200 @@ -66,7 +66,7 @@ /* controls */ def phase_text(phase: Session.Phase): String = - "Prover: " + Library.lowercase(phase.toString) + "Prover: " + Word.lowercase(phase.toString) private val session_phase = new Label(phase_text(PIDE.session.phase)) session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)