# HG changeset patch
# User wenzelm
# Date 1397398015 -7200
# Node ID 05c833d402bc2bafe401a52057e08ae90bd1ef05
# Parent  18d921496aa5820ad59b2a549a675a779416fcb9
tuned signature -- explicit Spell_Checker_Variable;

diff -r 18d921496aa5 -r 05c833d402bc src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sun Apr 13 15:34:54 2014 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sun Apr 13 16:06:55 2014 +0200
@@ -31,6 +31,7 @@
 
   val options = new JEdit_Options
   val completion_history = new Completion.History_Variable
+  val spell_checker = new Spell_Checker_Variable
 
   @volatile var startup_failure: Option[Throwable] = None
   @volatile var startup_notified = false
@@ -47,32 +48,6 @@
   lazy val editor = new JEdit_Editor
 
 
-  /* spell checker */
-
-  private val no_spell_checker: (String, Exn.Result[Spell_Checker]) =
-    ("", Exn.Exn(ERROR("No spell checker")))
-
-  @volatile private var current_spell_checker = no_spell_checker
-
-  def get_spell_checker: Option[Spell_Checker] =
-    current_spell_checker match {
-      case (_, Exn.Res(spell_checker)) => Some(spell_checker)
-      case _ => None
-    }
-
-  def update_spell_checker(): Unit =
-    if (options.bool("spell_checker")) {
-      val lang = options.string("spell_checker_language")
-      if (current_spell_checker._1 != lang) {
-        Spell_Checker.dictionaries.find(_.lang == lang) match {
-          case Some(dict) => current_spell_checker = (lang, Exn.capture { Spell_Checker(dict) })
-          case None => current_spell_checker = no_spell_checker
-        }
-      }
-    }
-    else current_spell_checker = no_spell_checker
-
-
   /* popups */
 
   def dismissed_popups(view: View): Boolean =
@@ -356,7 +331,7 @@
           }
 
         case msg: PropertiesChanged =>
-          PIDE.update_spell_checker()
+          PIDE.spell_checker.update(PIDE.options.value)
           PIDE.session.update_options(PIDE.options.value)
 
         case _ =>
@@ -375,7 +350,7 @@
 
       PIDE.options.update(Options.init())
       PIDE.completion_history.load()
-      PIDE.update_spell_checker()
+      PIDE.spell_checker.update(PIDE.options.value)
 
       SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
       if (ModeProvider.instance.isInstanceOf[ModeProvider])
diff -r 18d921496aa5 -r 05c833d402bc src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Sun Apr 13 15:34:54 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sun Apr 13 16:06:55 2014 +0200
@@ -319,7 +319,7 @@
 
             // spell-checker
             for {
-              spell_checker <- PIDE.get_spell_checker
+              spell_checker <- PIDE.spell_checker.get
               range0 <- rendering.spell_checker_ranges(line_range)
               text <- JEdit_Lib.try_get_text(buffer, range0)
               range <- spell_checker.bad_words(text)
diff -r 18d921496aa5 -r 05c833d402bc src/Tools/jEdit/src/spell_checker.scala
--- a/src/Tools/jEdit/src/spell_checker.scala	Sun Apr 13 15:34:54 2014 +0200
+++ b/src/Tools/jEdit/src/spell_checker.scala	Sun Apr 13 16:06:55 2014 +0200
@@ -115,3 +115,31 @@
   }
 }
 
+
+class Spell_Checker_Variable
+{
+  private val no_spell_checker: (String, Option[Spell_Checker]) = ("", None)
+  private var current_spell_checker = no_spell_checker
+
+  def get: Option[Spell_Checker] = synchronized { current_spell_checker._2 }
+
+  def update(options: Options): Unit = synchronized {
+    if (options.bool("spell_checker")) {
+      val lang = options.string("spell_checker_language")
+      if (current_spell_checker._1 != lang) {
+        Spell_Checker.dictionaries.find(_.lang == lang) match {
+          case Some(dict) =>
+            val spell_checker =
+              Exn.capture { Spell_Checker(dict) } match {
+                case Exn.Res(spell_checker) => Some(spell_checker)
+                case Exn.Exn(_) => None
+              }
+            current_spell_checker = (lang, spell_checker)
+          case None =>
+            current_spell_checker = no_spell_checker
+        }
+      }
+    }
+    else current_spell_checker = no_spell_checker
+  }
+}