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