# HG changeset patch
# User wenzelm
# Date 1397396094 -7200
# Node ID 18d921496aa5820ad59b2a549a675a779416fcb9
# Parent  347d7feae8d551a9c2afec8f129f9691e5011251
updated to jortho-1.0-1: dictionaries from SCOWL 7.1, with parameters like aspell;
simplified dictionary file format;
tuned signature;

diff -r 347d7feae8d5 -r 18d921496aa5 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Sun Apr 13 15:32:03 2014 +0200
+++ b/Admin/components/components.sha1	Sun Apr 13 15:34:54 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
+c8a19a36adf6cefa779d85f22ded2f4654e68ea5  jortho-1.0-1.tar.gz
 ffe179867cf5ffaabbb6bb096db9bdc0d7110065  jortho-1.0.tar.gz
 6c737137cc597fc920943783382e928ea79e3feb  kodkodi-1.2.16.tar.gz
 5f95c96bb99927f3a026050f85bd056f37a9189e  kodkodi-1.5.2.tar.gz
diff -r 347d7feae8d5 -r 18d921496aa5 Admin/components/main
--- a/Admin/components/main	Sun Apr 13 15:32:03 2014 +0200
+++ b/Admin/components/main	Sun Apr 13 15:34:54 2014 +0200
@@ -6,7 +6,7 @@
 jdk-7u40
 jedit_build-20140405
 jfreechart-1.0.14-1
-jortho-1.0
+jortho-1.0-1
 kodkodi-1.5.2
 polyml-5.5.1-1
 scala-2.10.4
diff -r 347d7feae8d5 -r 18d921496aa5 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sun Apr 13 15:32:03 2014 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sun Apr 13 15:34:54 2014 +0200
@@ -63,8 +63,12 @@
   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) })
+      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
 
diff -r 347d7feae8d5 -r 18d921496aa5 src/Tools/jEdit/src/spell_checker.scala
--- a/src/Tools/jEdit/src/spell_checker.scala	Sun Apr 13 15:32:03 2014 +0200
+++ b/src/Tools/jEdit/src/spell_checker.scala	Sun Apr 13 15:34:54 2014 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Tools/jEdit/src/spell_checker.scala
     Author:     Makarius
 
-Spell-checker based on JOrtho (see http://sourceforge.net/projects/jortho).
+Spell checker based on JOrtho (see http://sourceforge.net/projects/jortho).
 */
 
 package isabelle.jedit
@@ -10,7 +10,6 @@
 import isabelle._
 
 import java.lang.Class
-import java.net.URL
 import java.util.Locale
 import java.text.BreakIterator
 
@@ -19,23 +18,37 @@
 
 object Spell_Checker
 {
-  def known_dictionaries: List[String] =
-    space_explode(',', Isabelle_System.getenv_strict("JORTHO_DICTIONARIES"))
+  class Dictionary private [Spell_Checker](path: Path)
+  {
+    val lang = path.split_ext._1.base.implode
+    override def toString: String = lang
+
+    val locale: Locale =
+      space_explode('_', lang) match {
+        case a :: _ => Locale.forLanguageTag(a)
+        case Nil => Locale.ENGLISH
+      }
 
-  def apply(lang: String): Spell_Checker =
-    if (known_dictionaries.contains(lang))
-      new Spell_Checker(
-        lang, Locale.forLanguageTag(lang),
-        classOf[com.inet.jortho.SpellChecker].getResource("dictionary_" + lang + ".ortho"))
-    else error("Unknown spell-checker dictionary for " + quote(lang))
+    def load_words: List[String] =
+      path.split_ext._2 match {
+        case "gz" => split_lines(File.read_gzip(path))
+        case "" => split_lines(File.read(path))
+        case ext => error("Bad file extension for dictionary " + path)
+      }
+  }
 
-  def apply(lang: String, locale: Locale, dict: URL): Spell_Checker =
-    new Spell_Checker(lang, locale, dict)
+  def dictionaries: List[Dictionary] =
+    for {
+      path <- Path.split(Isabelle_System.getenv("JORTHO_DICTIONARIES"))
+      if path.is_file
+    } yield new Dictionary(path)
+
+  def apply(dict: Dictionary): Spell_Checker = new Spell_Checker(dict)
 }
 
-class Spell_Checker private(lang: String, locale: Locale, dict: URL)
+class Spell_Checker private(dict: Spell_Checker.Dictionary)
 {
-  override def toString: String = "Spell_Checker(" + lang + ")"
+  override def toString: String = dict.toString
 
   private val dictionary =
   {
@@ -44,29 +57,15 @@
     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 add = factory_class.getDeclaredMethod("add", classOf[String])
+    add.setAccessible(true)
+    dict.load_words.foreach(add.invoke(factory, _))
 
     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])
@@ -83,9 +82,10 @@
 
   def check(word: String): Boolean =
     contains(word) ||
-    Library.is_all_caps(word) && contains(Library.lowercase(word, locale)) ||
+    Library.is_all_caps(word) && contains(Library.lowercase(word, dict.locale)) ||
     Library.is_capitalized(word) &&
-      (contains(Library.lowercase(word, locale)) || contains(Library.uppercase(word, locale)))
+      (contains(Library.lowercase(word, dict.locale)) ||
+       contains(Library.uppercase(word, dict.locale)))
 
   def complete(word: String): List[String] =
   {
@@ -99,7 +99,7 @@
   {
     val result = new mutable.ListBuffer[Text.Range]
 
-    val it = BreakIterator.getWordInstance(locale)
+    val it = BreakIterator.getWordInstance(dict.locale)
     it.setText(text)
 
     var i = 0