--- 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 =
--- 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)
--- /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(" ")
+}
+
--- 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('\\', '/')
}
--- 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
--- 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
--- 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
--- 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))
--- 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 =
--- 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
--- 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)
}
--- 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)