src/Pure/Tools/spell_checker.scala

+/*  Title:      Tools/jEdit/src/spell_checker.scala
+    Author:     Makarius
+
+Spell checker with completion, based on JOrtho (see
+http://sourceforge.net/projects/jortho).
+*/
+
+package isabelle
+
+
+import java.lang.Class
+
+import scala.collection.mutable
+import scala.annotation.tailrec
+import scala.collection.immutable.SortedMap
+
+
+object Spell_Checker
+{
+  /* words within text */
+
+  def marked_words(base: Text.Offset, text: String, mark: Text.Info[String] => Boolean)
+    : List[Text.Info[String]] =
+  {
+    val result = new mutable.ListBuffer[Text.Info[String]]
+    var offset = 0
+
+    def apostrophe(c: Int): Boolean =
+      c == '\'' && (offset + 1 == text.length || text(offset + 1) != '\'')
+
+    @tailrec def scan(pred: Int => Boolean)
+    {
+      if (offset < text.length) {
+        val c = text.codePointAt(offset)
+        if (pred(c)) {
+          offset += Character.charCount(c)
+          scan(pred)
+        }
+      }
+    }
+
+    while (offset < text.length) {
+      scan(c => !Character.isLetter(c))
+      val start = offset
+      scan(c => Character.isLetterOrDigit(c) || apostrophe(c))
+      val stop = offset
+      if (stop - start >= 2) {
+        val info = Text.Info(Text.Range(base + start, base + stop), text.substring(start, stop))
+        if (mark(info)) result += info
+      }
+    }
+    result.toList
+  }
+
+
+  /* dictionaries */
+
+  class Dictionary private[Spell_Checker](val path: Path)
+  {
+    val lang = path.split_ext._1.base.implode
+    val user_path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang)
+    override def toString: String = lang
+  }
+
+  private object Decl
+  {
+    def apply(name: String, include: Boolean): String =
+      if (include) name else "-" + name
+
+    def unapply(decl: String): Option[(String, Boolean)] =
+    {
+      val decl1 = decl.trim
+      if (decl1 == "" || decl1.startsWith("#")) None
+      else
+        Library.try_unprefix("-", decl1.trim) match {
+          case None => Some((decl1, true))
+          case Some(decl2) => Some((decl2, false))
+        }
+    }
+  }
+
+  def dictionaries(): List[Dictionary] =
+    for {
+      path <- Path.split(Isabelle_System.getenv("JORTHO_DICTIONARIES"))
+      if path.is_file
+    } yield new Dictionary(path)
+
+
+  /* create spell checker */
+
+  def apply(dictionary: Dictionary): Spell_Checker = new Spell_Checker(dictionary)
+
+  private sealed case class Update(include: Boolean, permanent: Boolean)
+}
+
+
+class Spell_Checker private(dictionary: Spell_Checker.Dictionary)
+{
+  override def toString: String = dictionary.toString
+
+
+  /* main dictionary content */
+
+  private var dict = new Object
+  private var updates = SortedMap.empty[String, Spell_Checker.Update]
+
+  private def included_iterator(): Iterator[String] =
+    for {
+      (word, upd) <- updates.iterator
+      if upd.include
+    } yield word
+
+  private def excluded(word: String): Boolean =
+    updates.get(word) match {
+      case Some(upd) => !upd.include
+      case None => false
+    }
+
+  private def load()
+  {
+    val main_dictionary = split_lines(File.read_gzip(dictionary.path))
+
+    val permanent_updates =
+      if (dictionary.user_path.is_file)
+        for {
+          Spell_Checker.Decl(word, include) <- split_lines(File.read(dictionary.user_path))
+        } yield (word, Spell_Checker.Update(include, true))
+      else Nil
+
+    updates =
+      updates -- (for ((name, upd) <- updates.iterator; if upd.permanent) yield name) ++
+        permanent_updates
+
+    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 add = Untyped.method(factory_class, "add", classOf[String])
+
+    for {
+      word <- main_dictionary.iterator ++ included_iterator()
+      if !excluded(word)
+    } add.invoke(factory, word)
+
+    dict = Untyped.method(factory_class, "create").invoke(factory)
+  }
+  load()
+
+  private def save()
+  {
+    val permanent_decls =
+      (for {
+        (word, upd) <- updates.iterator
+        if upd.permanent
+      } yield Spell_Checker.Decl(word, upd.include)).toList
+
+    if (permanent_decls.nonEmpty || dictionary.user_path.is_file) {
+      val header = """# User updates for spell-checker dictionary
+#
+#   * each line contains at most one word
+#   * extra blanks are ignored
+#   * lines starting with "#" are stripped
+#   * lines starting with "-" indicate excluded words
+#
+#:mode=text:encoding=UTF-8:
+
+"""
+      Isabelle_System.mkdirs(dictionary.user_path.expand.dir)
+      File.write(dictionary.user_path, header + cat_lines(permanent_decls))
+    }
+  }
+
+  def update(word: String, include: Boolean, permanent: Boolean)
+  {
+    updates += (word -> Spell_Checker.Update(include, permanent))
+
+    if (include) {
+      if (permanent) save()
+      Untyped.method(dict.getClass, "add", classOf[String]).invoke(dict, word)
+    }
+    else { save(); load() }
+  }
+
+  def reset()
+  {
+    updates = SortedMap.empty
+    load()
+  }
+
+  def reset_enabled(): Int =
+    updates.valuesIterator.filter(upd => !upd.permanent).length
+
+
+  /* check known words */
+
+  def contains(word: String): Boolean =
+    Untyped.method(dict.getClass.getSuperclass, "exist", classOf[String]).
+      invoke(dict, word).asInstanceOf[java.lang.Boolean].booleanValue
+
+  def check(word: String): Boolean =
+    word match {
+      case Word.Case(c) if c != Word.Lowercase =>
+        contains(word) || contains(Word.lowercase(word))
+      case _ =>
+        contains(word)
+    }
+
+  def marked_words(base: Text.Offset, text: String): List[Text.Info[String]] =
+    Spell_Checker.marked_words(base, text, info => !check(info.info))
+
+
+  /* suggestions for unknown words */
+
+  private def suggestions(word: String): Option[List[String]] =
+  {
+    val res =
+      Untyped.method(dict.getClass.getSuperclass, "searchSuggestions", classOf[String]).
+        invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
+    if (res.isEmpty) None else Some(res)
+  }
+
+  def complete(word: String): List[String] =
+    if (check(word)) Nil
+    else {
+      val word_case = Word.Case.unapply(word)
+      def recover_case(s: String) =
+        word_case match {
+          case Some(c) => Word.Case(c, s)
+          case None => s
+        }
+      val result =
+        word_case match {
+          case Some(c) if c != Word.Lowercase =>
+            suggestions(word) orElse suggestions(Word.lowercase(word))
+          case _ =>
+            suggestions(word)
+        }
+      result.getOrElse(Nil).map(recover_case)
+    }
+
+  def complete_enabled(word: String): Boolean = complete(word).nonEmpty
+}
+
+
+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_dictionary")
+      if (current_spell_checker._1 != lang) {
+        Spell_Checker.dictionaries.find(_.lang == lang) match {
+          case Some(dictionary) =>
+            val spell_checker =
+              Exn.capture { Spell_Checker(dictionary) } 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
+  }
+}