--- a/src/Pure/System/options.scala Sun Apr 13 16:06:55 2014 +0200
+++ b/src/Pure/System/options.scala Sun Apr 13 16:42:44 2014 +0200
@@ -50,7 +50,7 @@
def print: String = print(false)
def print_default: String = print(true)
- def title(strip: String): String =
+ def title(strip: String = ""): String =
{
val words = space_explode('_', name)
val words1 =
--- a/src/Tools/jEdit/etc/options Sun Apr 13 16:06:55 2014 +0200
+++ b/src/Tools/jEdit/etc/options Sun Apr 13 16:42:44 2014 +0200
@@ -54,8 +54,8 @@
public option spell_checker : bool = true
-- "enable spell-checker for prose words within document text, comments etc."
-public option spell_checker_language : string = "en"
- -- "language for spell-checker locale and dictionary (en, de, fr)"
+public option spell_checker_language : string = "en_US"
+ -- "language for spell-checker locale and dictionary"
public option spell_checker_elements : string = "words,comment,inner_comment,ML_comment,SML_comment"
-- "relevant markup elements for spell-checker, separated by commas"
--- a/src/Tools/jEdit/src/isabelle_options.scala Sun Apr 13 16:06:55 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala Sun Apr 13 16:42:44 2014 +0200
@@ -40,8 +40,12 @@
class Isabelle_Options1 extends Isabelle_Options("isabelle-general")
{
val options = PIDE.options
+
+ private val predefined =
+ List(Isabelle_Logic.logic_selector(false), Spell_Checker.dictionaries_selector())
+
protected val components =
- options.make_components(List(Isabelle_Logic.logic_selector(false)),
+ options.make_components(predefined,
(for ((name, opt) <- options.value.options.iterator if opt.public) yield name).toSet)
}
--- a/src/Tools/jEdit/src/spell_checker.scala Sun Apr 13 16:06:55 2014 +0200
+++ b/src/Tools/jEdit/src/spell_checker.scala Sun Apr 13 16:42:44 2014 +0200
@@ -14,10 +14,13 @@
import java.text.BreakIterator
import scala.collection.mutable
+import scala.swing.ComboBox
object Spell_Checker
{
+ /* dictionary consisting of word list */
+
class Dictionary private [Spell_Checker](path: Path)
{
val lang = path.split_ext._1.base.implode
@@ -25,7 +28,7 @@
val locale: Locale =
space_explode('_', lang) match {
- case a :: _ => Locale.forLanguageTag(a)
+ case l :: _ => Locale.forLanguageTag(l)
case Nil => Locale.ENGLISH
}
@@ -37,15 +40,49 @@
}
}
- def dictionaries: List[Dictionary] =
+
+ /* known dictionaries */
+
+ def dictionaries(): List[Dictionary] =
for {
path <- Path.split(Isabelle_System.getenv("JORTHO_DICTIONARIES"))
if path.is_file
} yield new Dictionary(path)
+ def dictionaries_selector(): Option_Component =
+ {
+ Swing_Thread.require()
+
+ val option_name = "spell_checker_language"
+ val opt = PIDE.options.value.check_name(option_name)
+
+ val entries = dictionaries()
+ val component = new ComboBox(entries) with Option_Component {
+ name = option_name
+ val title = opt.title()
+ def load: Unit =
+ {
+ val lang = PIDE.options.string(option_name)
+ entries.find(_.lang == lang) match {
+ case Some(entry) => selection.item = entry
+ case None =>
+ }
+ }
+ def save: Unit = PIDE.options.string(option_name) = selection.item.lang
+ }
+
+ component.load()
+ component.tooltip = opt.print_default
+ component
+ }
+
+
+ /* create spell checker */
+
def apply(dict: Dictionary): Spell_Checker = new Spell_Checker(dict)
}
+
class Spell_Checker private(dict: Spell_Checker.Dictionary)
{
override def toString: String = dict.toString