src/Tools/jEdit/src/spell_checker.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 64621 7116f2634e32
child 64882 c3b42ac0cf81
permissions -rw-r--r--
tuned signature;
     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 javax.swing.JMenuItem
    16 
    17 import scala.collection.mutable
    18 import scala.swing.ComboBox
    19 import scala.annotation.tailrec
    20 import scala.collection.immutable.SortedMap
    21 
    22 import org.gjt.sp.jedit.menu.EnhancedMenuItem
    23 import org.gjt.sp.jedit.{jEdit, Buffer}
    24 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
    25 
    26 
    27 object Spell_Checker
    28 {
    29   /** words within text **/
    30 
    31   def marked_words(base: Text.Offset, text: String, mark: Text.Info[String] => Boolean)
    32     : List[Text.Info[String]] =
    33   {
    34     val result = new mutable.ListBuffer[Text.Info[String]]
    35     var offset = 0
    36 
    37     def apostrophe(c: Int): Boolean =
    38       c == '\'' && (offset + 1 == text.length || text(offset + 1) != '\'')
    39 
    40     @tailrec def scan(pred: Int => Boolean)
    41     {
    42       if (offset < text.length) {
    43         val c = text.codePointAt(offset)
    44         if (pred(c)) {
    45           offset += Character.charCount(c)
    46           scan(pred)
    47         }
    48       }
    49     }
    50 
    51     while (offset < text.length) {
    52       scan(c => !Character.isLetter(c))
    53       val start = offset
    54       scan(c => Character.isLetterOrDigit(c) || apostrophe(c))
    55       val stop = offset
    56       if (stop - start >= 2) {
    57         val info = Text.Info(Text.Range(base + start, base + stop), text.substring(start, stop))
    58         if (mark(info)) result += info
    59       }
    60     }
    61     result.toList
    62   }
    63 
    64   def current_word(text_area: TextArea, rendering: JEdit_Rendering, range: Text.Range)
    65     : Option[Text.Info[String]] =
    66   {
    67     for {
    68       spell_range <- rendering.spell_checker_point(range)
    69       text <- JEdit_Lib.try_get_text(text_area.getBuffer, spell_range)
    70       info <- marked_words(spell_range.start, text, info => info.range.overlaps(range)).headOption
    71     } yield info
    72   }
    73 
    74 
    75 
    76   /** completion **/
    77 
    78   def completion(text_area: TextArea, explicit: Boolean, rendering: JEdit_Rendering)
    79       : Option[Completion.Result] =
    80   {
    81     for {
    82       spell_checker <- PIDE.spell_checker.get
    83       if explicit
    84       range = JEdit_Lib.before_caret_range(text_area, rendering)
    85       word <- current_word(text_area, rendering, range)
    86       words = spell_checker.complete(word.info)
    87       if words.nonEmpty
    88       descr = "(from dictionary " + quote(spell_checker.toString) + ")"
    89       items =
    90         words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false))
    91     } yield Completion.Result(word.range, word.info, false, items)
    92   }
    93 
    94 
    95 
    96   /** context menu **/
    97 
    98   def context_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] =
    99   {
   100     val result =
   101       for {
   102         spell_checker <- PIDE.spell_checker.get
   103         doc_view <- PIDE.document_view(text_area)
   104         rendering = doc_view.get_rendering()
   105         range = JEdit_Lib.point_range(text_area.getBuffer, offset)
   106         Text.Info(_, word) <- current_word(text_area, rendering, range)
   107       } yield (spell_checker, word)
   108 
   109     result match {
   110       case Some((spell_checker, word)) =>
   111 
   112         val context = jEdit.getActionContext()
   113         def item(name: String): JMenuItem =
   114           new EnhancedMenuItem(context.getAction(name).getLabel, name, context)
   115 
   116         val complete_items =
   117           if (spell_checker.complete_enabled(word)) List(item("isabelle.complete-word"))
   118           else Nil
   119 
   120         val update_items =
   121           if (spell_checker.check(word))
   122             List(item("isabelle.exclude-word"), item("isabelle.exclude-word-permanently"))
   123           else
   124             List(item("isabelle.include-word"), item("isabelle.include-word-permanently"))
   125 
   126         val reset_items =
   127           spell_checker.reset_enabled() match {
   128             case 0 => Nil
   129             case n =>
   130               val name = "isabelle.reset-words"
   131               val label = context.getAction(name).getLabel
   132               List(new EnhancedMenuItem(label + " (" + n + ")", name, context))
   133           }
   134 
   135         complete_items ::: update_items ::: reset_items
   136 
   137       case None => Nil
   138     }
   139   }
   140 
   141 
   142 
   143   /** dictionary **/
   144 
   145   /* declarations */
   146 
   147   class Dictionary private[Spell_Checker](val path: Path)
   148   {
   149     val lang = path.split_ext._1.base.implode
   150     val user_path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang)
   151     override def toString: String = lang
   152   }
   153 
   154   private object Decl
   155   {
   156     def apply(name: String, include: Boolean): String =
   157       if (include) name else "-" + name
   158 
   159     def unapply(decl: String): Option[(String, Boolean)] =
   160     {
   161       val decl1 = decl.trim
   162       if (decl1 == "" || decl1.startsWith("#")) None
   163       else
   164         Library.try_unprefix("-", decl1.trim) match {
   165           case None => Some((decl1, true))
   166           case Some(decl2) => Some((decl2, false))
   167         }
   168     }
   169   }
   170 
   171 
   172   /* known dictionaries */
   173 
   174   def dictionaries(): List[Dictionary] =
   175     for {
   176       path <- Path.split(Isabelle_System.getenv("JORTHO_DICTIONARIES"))
   177       if path.is_file
   178     } yield new Dictionary(path)
   179 
   180   def dictionaries_selector(): Option_Component =
   181   {
   182     GUI_Thread.require {}
   183 
   184     val option_name = "spell_checker_dictionary"
   185     val opt = PIDE.options.value.check_name(option_name)
   186 
   187     val entries = dictionaries()
   188     val component = new ComboBox(entries) with Option_Component {
   189       name = option_name
   190       val title = opt.title()
   191       def load: Unit =
   192       {
   193         val lang = PIDE.options.string(option_name)
   194         entries.find(_.lang == lang) match {
   195           case Some(entry) => selection.item = entry
   196           case None =>
   197         }
   198       }
   199       def save: Unit = PIDE.options.string(option_name) = selection.item.lang
   200     }
   201 
   202     component.load()
   203     component.tooltip = GUI.tooltip_lines(opt.print_default)
   204     component
   205   }
   206 
   207 
   208   /* create spell checker */
   209 
   210   def apply(dictionary: Dictionary): Spell_Checker = new Spell_Checker(dictionary)
   211 
   212   private sealed case class Update(include: Boolean, permanent: Boolean)
   213 }
   214 
   215 
   216 class Spell_Checker private(dictionary: Spell_Checker.Dictionary)
   217 {
   218   override def toString: String = dictionary.toString
   219 
   220 
   221   /* main dictionary content */
   222 
   223   private var dict = new Object
   224   private var updates = SortedMap.empty[String, Spell_Checker.Update]
   225 
   226   private def included_iterator(): Iterator[String] =
   227     for {
   228       (word, upd) <- updates.iterator
   229       if upd.include
   230     } yield word
   231 
   232   private def excluded(word: String): Boolean =
   233     updates.get(word) match {
   234       case Some(upd) => !upd.include
   235       case None => false
   236     }
   237 
   238   private def load()
   239   {
   240     val main_dictionary = split_lines(File.read_gzip(dictionary.path))
   241 
   242     val permanent_updates =
   243       if (dictionary.user_path.is_file)
   244         for {
   245           Spell_Checker.Decl(word, include) <- split_lines(File.read(dictionary.user_path))
   246         } yield (word, Spell_Checker.Update(include, true))
   247       else Nil
   248 
   249     updates =
   250       updates -- (for ((name, upd) <- updates.iterator; if upd.permanent) yield name) ++
   251         permanent_updates
   252 
   253     val factory_class = Class.forName("com.inet.jortho.DictionaryFactory")
   254     val factory_cons = factory_class.getConstructor()
   255     factory_cons.setAccessible(true)
   256     val factory = factory_cons.newInstance()
   257 
   258     val add = Untyped.method(factory_class, "add", classOf[String])
   259 
   260     for {
   261       word <- main_dictionary.iterator ++ included_iterator()
   262       if !excluded(word)
   263     } add.invoke(factory, word)
   264 
   265     dict = Untyped.method(factory_class, "create").invoke(factory)
   266   }
   267   load()
   268 
   269   private def save()
   270   {
   271     val permanent_decls =
   272       (for {
   273         (word, upd) <- updates.iterator
   274         if upd.permanent
   275       } yield Spell_Checker.Decl(word, upd.include)).toList
   276 
   277     if (permanent_decls.nonEmpty || dictionary.user_path.is_file) {
   278       val header = """# User updates for spell-checker dictionary
   279 #
   280 #   * each line contains at most one word
   281 #   * extra blanks are ignored
   282 #   * lines starting with "#" are stripped
   283 #   * lines starting with "-" indicate excluded words
   284 #
   285 #:mode=text:encoding=UTF-8:
   286 
   287 """
   288       Isabelle_System.mkdirs(dictionary.user_path.expand.dir)
   289       File.write(dictionary.user_path, header + cat_lines(permanent_decls))
   290     }
   291   }
   292 
   293   def update(word: String, include: Boolean, permanent: Boolean)
   294   {
   295     updates += (word -> Spell_Checker.Update(include, permanent))
   296 
   297     if (include) {
   298       if (permanent) save()
   299       Untyped.method(dict.getClass, "add", classOf[String]).invoke(dict, word)
   300     }
   301     else { save(); load() }
   302   }
   303 
   304   def reset()
   305   {
   306     updates = SortedMap.empty
   307     load()
   308   }
   309 
   310   def reset_enabled(): Int =
   311     updates.valuesIterator.filter(upd => !upd.permanent).length
   312 
   313 
   314   /* check known words */
   315 
   316   def contains(word: String): Boolean =
   317     Untyped.method(dict.getClass.getSuperclass, "exist", classOf[String]).
   318       invoke(dict, word).asInstanceOf[java.lang.Boolean].booleanValue
   319 
   320   def check(word: String): Boolean =
   321     word match {
   322       case Word.Case(c) if c != Word.Lowercase =>
   323         contains(word) || contains(Word.lowercase(word))
   324       case _ =>
   325         contains(word)
   326     }
   327 
   328   def marked_words(base: Text.Offset, text: String): List[Text.Info[String]] =
   329     Spell_Checker.marked_words(base, text, info => !check(info.info))
   330 
   331 
   332   /* suggestions for unknown words */
   333 
   334   private def suggestions(word: String): Option[List[String]] =
   335   {
   336     val res =
   337       Untyped.method(dict.getClass.getSuperclass, "searchSuggestions", classOf[String]).
   338         invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
   339     if (res.isEmpty) None else Some(res)
   340   }
   341 
   342   def complete(word: String): List[String] =
   343     if (check(word)) Nil
   344     else {
   345       val word_case = Word.Case.unapply(word)
   346       def recover_case(s: String) =
   347         word_case match {
   348           case Some(c) => Word.Case(c, s)
   349           case None => s
   350         }
   351       val result =
   352         word_case match {
   353           case Some(c) if c != Word.Lowercase =>
   354             suggestions(word) orElse suggestions(Word.lowercase(word))
   355           case _ =>
   356             suggestions(word)
   357         }
   358       result.getOrElse(Nil).map(recover_case)
   359     }
   360 
   361   def complete_enabled(word: String): Boolean = complete(word).nonEmpty
   362 }
   363 
   364 
   365 class Spell_Checker_Variable
   366 {
   367   private val no_spell_checker: (String, Option[Spell_Checker]) = ("", None)
   368   private var current_spell_checker = no_spell_checker
   369 
   370   def get: Option[Spell_Checker] = synchronized { current_spell_checker._2 }
   371 
   372   def update(options: Options): Unit = synchronized {
   373     if (options.bool("spell_checker")) {
   374       val lang = options.string("spell_checker_dictionary")
   375       if (current_spell_checker._1 != lang) {
   376         Spell_Checker.dictionaries.find(_.lang == lang) match {
   377           case Some(dictionary) =>
   378             val spell_checker =
   379               Exn.capture { Spell_Checker(dictionary) } match {
   380                 case Exn.Res(spell_checker) => Some(spell_checker)
   381                 case Exn.Exn(_) => None
   382               }
   383             current_spell_checker = (lang, spell_checker)
   384           case None =>
   385             current_spell_checker = no_spell_checker
   386         }
   387       }
   388     }
   389     else current_spell_checker = no_spell_checker
   390   }
   391 }
   392