# HG changeset patch
# User wenzelm
# Date 1397400164 -7200
# Node ID eece73c31e384fe68134c9bde46001431674a9a5
# Parent  05c833d402bc2bafe401a52057e08ae90bd1ef05
added dictionaries_selector GUI;
tuned;

diff -r 05c833d402bc -r eece73c31e38 src/Pure/System/options.scala
--- 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 =
diff -r 05c833d402bc -r eece73c31e38 src/Tools/jEdit/etc/options
--- 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"
diff -r 05c833d402bc -r eece73c31e38 src/Tools/jEdit/src/isabelle_options.scala
--- 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)
 }
 
diff -r 05c833d402bc -r eece73c31e38 src/Tools/jEdit/src/spell_checker.scala
--- 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