added spell-checker options;
support for rendering bad words;

--- a/src/Tools/jEdit/etc/options	Sat Apr 12 18:55:49 2014 +0200
+++ b/src/Tools/jEdit/etc/options	Sat Apr 12 20:49:57 2014 +0200
@@ -49,6 +49,15 @@
   -- "insert uniquely completed abbreviation immediately into buffer"
 
 
+section "Spell Checker"
+
+public option spell_checker : bool = true
+  -- "enable spell-checker for prose words within document text"
+
+public option spell_checker_language : string = "en"
+  -- "language for spell-checker locale and dictionary (en, de, fr)"
+
+
 section "Rendering of Document Content"
 
 option outdated_color : string = "EEE3E3FF"
@@ -68,6 +77,7 @@
 option tracing_message_color : string = "F0F8FFFF"
 option warning_message_color : string = "EEE8AAFF"
 option error_message_color : string = "FFC1C1FF"
+option spell_checker_color : string = "B22222FF"
 option bad_color : string = "FF6A6A64"
 option intensify_color : string = "FFCC6664"
 option quoted_color : string = "8B8B8B19"

--- a/src/Tools/jEdit/src/plugin.scala	Sat Apr 12 18:55:49 2014 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sat Apr 12 20:49:57 2014 +0200
@@ -47,6 +47,28 @@
   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)
+        current_spell_checker = (lang, Exn.capture { Spell_Checker(lang) })
+    }
+    else current_spell_checker = no_spell_checker
+
+
   /* popups */
 
   def dismissed_popups(view: View): Boolean =
@@ -330,6 +352,7 @@
           }
 
         case msg: PropertiesChanged =>
+          PIDE.update_spell_checker()
           PIDE.session.update_options(PIDE.options.value)
 
         case _ =>
@@ -348,6 +371,7 @@
 
       PIDE.options.update(Options.init())
       PIDE.completion_history.load()
+      PIDE.update_spell_checker()
 
       SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
       if (ModeProvider.instance.isInstanceOf[ModeProvider])

--- a/src/Tools/jEdit/src/rendering.scala	Sat Apr 12 18:55:49 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Apr 12 20:49:57 2014 +0200
@@ -227,6 +227,7 @@
   val tracing_message_color = color_value("tracing_message_color")
   val warning_message_color = color_value("warning_message_color")
   val error_message_color = color_value("error_message_color")
+  val spell_checker_color = color_value("spell_checker_color")
   val bad_color = color_value("bad_color")
   val intensify_color = color_value("intensify_color")
   val quoted_color = color_value("quoted_color")

--- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Apr 12 18:55:49 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Apr 12 20:49:57 2014 +0200
@@ -316,6 +316,19 @@
                 gfx.drawLine(x1, y1, x1 + 1, y1)
               }
             }
+
+            // spell-checker
+            for {
+              spell_checker <- PIDE.get_spell_checker
+              range0 <- rendering.prose_words(line_range).iterator
+              text <- JEdit_Lib.try_get_text(buffer, range0)
+              range <- spell_checker.bad_words(text)
+              r <- JEdit_Lib.gfx_range(text_area, range + range0.start)
+            } {
+              gfx.setColor(rendering.spell_checker_color)
+              val y0 = r.y + fm.getAscent + 2
+              gfx.drawLine(r.x, y0, r.x + r.length, y0)
+            }
           }
         }
       }