src/Tools/jEdit/src/spell_checker.scala
author wenzelm
Wed Jul 23 11:19:24 2014 +0200 (2014-07-23 ago)
changeset 57612 990ffb84489b
parent 56662 f373fb77e0a4
child 58549 d4d97b79f1fb
permissions -rw-r--r--
clarified module name: facilitate alternative GUI frameworks;
     1 /*  Title:      Tools/jEdit/src/spell_checker.scala
     2     Author:     Makarius
     3 
     4 Spell checker with completion, based on JOrtho (see
     5 http://sourceforge.net/projects/jortho).
     6 */
     7 
     8 package isabelle.jedit
     9 
    10 
    11 import isabelle._
    12 
    13 import java.lang.Class
    14 
    15 import scala.collection.mutable
    16 import scala.swing.ComboBox
    17 import scala.annotation.tailrec
    18 import scala.collection.immutable.SortedMap
    19 
    20 import org.gjt.sp.jedit.textarea.TextArea
    21 
    22 
    23 object Spell_Checker
    24 {
    25   /* words within text */
    26 
    27   def marked_words(base: Text.Offset, text: String, mark: Text.Info[String] => Boolean)
    28     : List[Text.Info[String]] =
    29   {
    30     val result = new mutable.ListBuffer[Text.Info[String]]
    31     var offset = 0
    32 
    33     def apostrophe(c: Int): Boolean =
    34       c == '\'' && (offset + 1 == text.length || text(offset + 1) != '\'')
    35 
    36     @tailrec def scan(pred: Int => Boolean)
    37     {
    38       if (offset < text.length) {
    39         val c = text.codePointAt(offset)
    40         if (pred(c)) {
    41           offset += Character.charCount(c)
    42           scan(pred)
    43         }
    44       }
    45     }
    46 
    47     while (offset < text.length) {
    48       scan(c => !Character.isLetter(c))
    49       val start = offset
    50       scan(c => Character.isLetterOrDigit(c) || apostrophe(c))
    51       val stop = offset
    52       if (stop - start >= 2) {
    53         val info = Text.Info(Text.Range(base + start, base + stop), text.substring(start, stop))
    54         if (mark(info)) result += info
    55       }
    56     }
    57     result.toList
    58   }
    59 
    60   def current_word(text_area: TextArea, rendering: Rendering, range: Text.Range)
    61     : Option[Text.Info[String]] =
    62   {
    63     for {
    64       spell_range <- rendering.spell_checker_point(range)
    65       text <- JEdit_Lib.try_get_text(text_area.getBuffer, spell_range)
    66       info <- marked_words(spell_range.start, text, info => info.range.overlaps(range)).headOption
    67     } yield info
    68   }
    69 
    70 
    71   /* dictionary declarations */
    72 
    73   class Dictionary private[Spell_Checker](val path: Path)
    74   {
    75     val lang = path.split_ext._1.base.implode
    76     val user_path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang)
    77     override def toString: String = lang
    78   }
    79 
    80   private object Decl
    81   {
    82     def apply(name: String, include: Boolean): String =
    83       if (include) name else "-" + name
    84 
    85     def unapply(decl: String): Option[(String, Boolean)] =
    86     {
    87       val decl1 = decl.trim
    88       if (decl1 == "" || decl1.startsWith("#")) None
    89       else
    90         Library.try_unprefix("-", decl1.trim) match {
    91           case None => Some((decl1, true))
    92           case Some(decl2) => Some((decl2, false))
    93         }
    94     }
    95   }
    96 
    97 
    98   /* known dictionaries */
    99 
   100   def dictionaries(): List[Dictionary] =
   101     for {
   102       path <- Path.split(Isabelle_System.getenv("JORTHO_DICTIONARIES"))
   103       if path.is_file
   104     } yield new Dictionary(path)
   105 
   106   def dictionaries_selector(): Option_Component =
   107   {
   108     GUI_Thread.require {}
   109 
   110     val option_name = "spell_checker_dictionary"
   111     val opt = PIDE.options.value.check_name(option_name)
   112 
   113     val entries = dictionaries()
   114     val component = new ComboBox(entries) with Option_Component {
   115       name = option_name
   116       val title = opt.title()
   117       def load: Unit =
   118       {
   119         val lang = PIDE.options.string(option_name)
   120         entries.find(_.lang == lang) match {
   121           case Some(entry) => selection.item = entry
   122           case None =>
   123         }
   124       }
   125       def save: Unit = PIDE.options.string(option_name) = selection.item.lang
   126     }
   127 
   128     component.load()
   129     component.tooltip = GUI.tooltip_lines(opt.print_default)
   130     component
   131   }
   132 
   133 
   134   /* create spell checker */
   135 
   136   def apply(dictionary: Dictionary): Spell_Checker = new Spell_Checker(dictionary)
   137 
   138   private sealed case class Update(include: Boolean, permanent: Boolean)
   139 }
   140 
   141 
   142 class Spell_Checker private(dictionary: Spell_Checker.Dictionary)
   143 {
   144   override def toString: String = dictionary.toString
   145 
   146 
   147   /* main dictionary content */
   148 
   149   private var dict = new Object
   150   private var updates = SortedMap.empty[String, Spell_Checker.Update]
   151 
   152   private def included_iterator(): Iterator[String] =
   153     for {
   154       (word, upd) <- updates.iterator
   155       if upd.include
   156     } yield word
   157 
   158   private def excluded(word: String): Boolean =
   159     updates.get(word) match {
   160       case Some(upd) => !upd.include
   161       case None => false
   162     }
   163 
   164   private def load()
   165   {
   166     val main_dictionary = split_lines(File.read_gzip(dictionary.path))
   167 
   168     val permanent_updates =
   169       if (dictionary.user_path.is_file)
   170         for {
   171           Spell_Checker.Decl(word, include) <- split_lines(File.read(dictionary.user_path))
   172         } yield (word, Spell_Checker.Update(include, true))
   173       else Nil
   174 
   175     updates =
   176       updates -- (for ((name, upd) <- updates.iterator; if upd.permanent) yield name) ++
   177         permanent_updates
   178 
   179     val factory_class = Class.forName("com.inet.jortho.DictionaryFactory")
   180     val factory_cons = factory_class.getConstructor()
   181     factory_cons.setAccessible(true)
   182     val factory = factory_cons.newInstance()
   183 
   184     val add = factory_class.getDeclaredMethod("add", classOf[String])
   185     add.setAccessible(true)
   186 
   187     for {
   188       word <- main_dictionary.iterator ++ included_iterator()
   189       if !excluded(word)
   190     } add.invoke(factory, word)
   191 
   192     val create = factory_class.getDeclaredMethod("create")
   193     create.setAccessible(true)
   194     dict = create.invoke(factory)
   195   }
   196   load()
   197 
   198   private def save()
   199   {
   200     val permanent_decls =
   201       (for {
   202         (word, upd) <- updates.iterator
   203         if upd.permanent
   204       } yield Spell_Checker.Decl(word, upd.include)).toList
   205 
   206     if (!permanent_decls.isEmpty || dictionary.user_path.is_file) {
   207       val header = """# User updates for spell-checker dictionary
   208 #
   209 #   * each line contains at most one word
   210 #   * extra blanks are ignored
   211 #   * lines starting with "#" are stripped
   212 #   * lines starting with "-" indicate excluded words
   213 #
   214 #:mode=text:encoding=UTF-8:
   215 
   216 """
   217       Isabelle_System.mkdirs(dictionary.user_path.expand.dir)
   218       File.write(dictionary.user_path, header + cat_lines(permanent_decls))
   219     }
   220   }
   221 
   222   def update(word: String, include: Boolean, permanent: Boolean)
   223   {
   224     updates += (word -> Spell_Checker.Update(include, permanent))
   225 
   226     if (include) {
   227       if (permanent) save()
   228 
   229       val m = dict.getClass.getDeclaredMethod("add", classOf[String])
   230       m.setAccessible(true)
   231       m.invoke(dict, word)
   232     }
   233     else { save(); load() }
   234   }
   235 
   236   def reset()
   237   {
   238     updates = SortedMap.empty
   239     load()
   240   }
   241 
   242   def reset_enabled(): Int =
   243     updates.valuesIterator.filter(upd => !upd.permanent).length
   244 
   245 
   246   /* check known words */
   247 
   248   def contains(word: String): Boolean =
   249   {
   250     val m = dict.getClass.getSuperclass.getDeclaredMethod("exist", classOf[String])
   251     m.setAccessible(true)
   252     m.invoke(dict, word).asInstanceOf[java.lang.Boolean].booleanValue
   253   }
   254 
   255   def check(word: String): Boolean =
   256     word match {
   257       case Word.Case(c) if c != Word.Lowercase =>
   258         contains(word) || contains(Word.lowercase(word))
   259       case _ =>
   260         contains(word)
   261     }
   262 
   263   def marked_words(base: Text.Offset, text: String): List[Text.Info[String]] =
   264     Spell_Checker.marked_words(base, text, info => !check(info.info))
   265 
   266 
   267   /* suggestions for unknown words */
   268 
   269   private def suggestions(word: String): Option[List[String]] =
   270   {
   271     val m = dict.getClass.getSuperclass.getDeclaredMethod("searchSuggestions", classOf[String])
   272     m.setAccessible(true)
   273     val res =
   274       m.invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
   275     if (res.isEmpty) None else Some(res)
   276   }
   277 
   278   def complete(word: String): List[String] =
   279     if (check(word)) Nil
   280     else {
   281       val word_case = Word.Case.unapply(word)
   282       def recover_case(s: String) =
   283         word_case match {
   284           case Some(c) => Word.Case(c, s)
   285           case None => s
   286         }
   287       val result =
   288         word_case match {
   289           case Some(c) if c != Word.Lowercase =>
   290             suggestions(word) orElse suggestions(Word.lowercase(word))
   291           case _ =>
   292             suggestions(word)
   293         }
   294       result.getOrElse(Nil).map(recover_case)
   295     }
   296 
   297   def complete_enabled(word: String): Boolean = !complete(word).isEmpty
   298 }
   299 
   300 
   301 class Spell_Checker_Variable
   302 {
   303   private val no_spell_checker: (String, Option[Spell_Checker]) = ("", None)
   304   private var current_spell_checker = no_spell_checker
   305 
   306   def get: Option[Spell_Checker] = synchronized { current_spell_checker._2 }
   307 
   308   def update(options: Options): Unit = synchronized {
   309     if (options.bool("spell_checker")) {
   310       val lang = options.string("spell_checker_dictionary")
   311       if (current_spell_checker._1 != lang) {
   312         Spell_Checker.dictionaries.find(_.lang == lang) match {
   313           case Some(dictionary) =>
   314             val spell_checker =
   315               Exn.capture { Spell_Checker(dictionary) } match {
   316                 case Exn.Res(spell_checker) => Some(spell_checker)
   317                 case Exn.Exn(_) => None
   318               }
   319             current_spell_checker = (lang, spell_checker)
   320           case None =>
   321             current_spell_checker = no_spell_checker
   322         }
   323       }
   324     }
   325     else current_spell_checker = no_spell_checker
   326   }
   327 }
   328