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