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