added spell-checker based on jortho-1.0;

--- a/Admin/components/components.sha1	Fri Apr 11 19:07:56 2014 +0200
+++ b/Admin/components/components.sha1	Fri Apr 11 23:26:31 2014 +0200
@@ -42,6 +42,7 @@
 054c1300128f8abd0f46a3e92c756ccdb96ff2af  jedit_build-20140405.tar.gz
 0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa  jfreechart-1.0.14-1.tar.gz
 8122526f1fc362ddae1a328bdbc2152853186fee  jfreechart-1.0.14.tar.gz
+ffe179867cf5ffaabbb6bb096db9bdc0d7110065  jortho-1.0.tar.gz
 6c737137cc597fc920943783382e928ea79e3feb  kodkodi-1.2.16.tar.gz
 5f95c96bb99927f3a026050f85bd056f37a9189e  kodkodi-1.5.2.tar.gz
 377e36efb8608e6c828c7718d890e97fde2006a4  linux_app-20131007.tar.gz

--- a/Admin/components/main	Fri Apr 11 19:07:56 2014 +0200
+++ b/Admin/components/main	Fri Apr 11 23:26:31 2014 +0200
@@ -6,6 +6,7 @@
 jdk-7u40
 jedit_build-20140405
 jfreechart-1.0.14-1
+jortho-1.0
 kodkodi-1.5.2
 polyml-5.5.1-1
 scala-2.10.4

--- a/src/Tools/jEdit/lib/Tools/jedit	Fri Apr 11 19:07:56 2014 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Apr 11 23:26:31 2014 +0200
@@ -42,6 +42,7 @@
   "src/sledgehammer_dockable.scala"
   "src/simplifier_trace_dockable.scala"
   "src/simplifier_trace_window.scala"
+  "src/spell_checker.scala"
   "src/symbols_dockable.scala"
   "src/syslog_dockable.scala"
   "src/text_overview.scala"

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/spell_checker.scala	Fri Apr 11 23:26:31 2014 +0200
@@ -0,0 +1,87 @@
+/*  Title:      Tools/jEdit/src/spell_checker.scala
+    Author:     Makarius
+
+Spell-checker based on JOrtho (see http://sourceforge.net/projects/jortho).
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.lang.Class
+import java.net.URL
+
+
+object Spell_Checker
+{
+  def known_dictionaries: List[String] =
+    space_explode(',', Isabelle_System.getenv_strict("JORTHO_DICTIONARIES"))
+
+  def apply(dict: String): Spell_Checker =
+    if (known_dictionaries.contains(dict))
+      new Spell_Checker(
+        dict, classOf[com.inet.jortho.SpellChecker].getResource("dictionary_" + dict + ".ortho"))
+    else error("Unknown spell-checker dictionary " + quote(dict))
+
+  def apply(dict: URL): Spell_Checker =
+    new Spell_Checker(dict.toString, dict)
+}
+
+class Spell_Checker private(dict_name: String, dict: URL)
+{
+  override def toString: String = "Spell_Checker(" + dict_name + ")"
+
+  private val dictionary =
+  {
+    val factory_class = Class.forName("com.inet.jortho.DictionaryFactory")
+    val factory_cons = factory_class.getConstructor()
+    factory_cons.setAccessible(true)
+    val factory = factory_cons.newInstance()
+
+    val load_word_list = factory_class.getDeclaredMethod("loadWordList", classOf[URL])
+    load_word_list.setAccessible(true)
+    load_word_list.invoke(factory, dict)
+
+    val create = factory_class.getDeclaredMethod("create")
+    create.setAccessible(true)
+    create.invoke(factory)
+  }
+
+  def load(file_name: String)
+  {
+    val m = dictionary.getClass.getDeclaredMethod("load", classOf[String])
+    m.setAccessible(true)
+    m.invoke(dictionary, file_name)
+  }
+
+  def save(file_name: String)
+  {
+    val m = dictionary.getClass.getDeclaredMethod("save", classOf[String])
+    m.setAccessible(true)
+    m.invoke(dictionary, file_name)
+  }
+
+  def add(word: String)
+  {
+    val m = dictionary.getClass.getDeclaredMethod("add", classOf[String])
+    m.setAccessible(true)
+    m.invoke(dictionary, word)
+  }
+
+  def check(word: String): Boolean =
+  {
+    val m = dictionary.getClass.getSuperclass.getDeclaredMethod("exist", classOf[String])
+    m.setAccessible(true)
+    m.invoke(dictionary, word).asInstanceOf[java.lang.Boolean].booleanValue
+  }
+
+  def complete(word: String): List[String] =
+  {
+    val m = dictionary.getClass.getSuperclass.
+      getDeclaredMethod("searchSuggestions", classOf[String])
+    m.setAccessible(true)
+    m.invoke(dictionary, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
+  }
+}
+