src/Tools/jEdit/src/spell_checker.scala
author wenzelm
Tue, 15 Apr 2014 00:23:15 +0200
changeset 56583 c49607db182a
parent 56581 af3e6576e680
child 56584 9ccbac38bcad
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56547
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/jEdit/src/spell_checker.scala
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
     3
56567
wenzelm
parents: 56566
diff changeset
     4
Spell checker with completion, based on JOrtho (see
wenzelm
parents: 56566
diff changeset
     5
http://sourceforge.net/projects/jortho).
56547
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
     6
*/
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
     7
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
     8
package isabelle.jedit
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
     9
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
    10
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
    11
import isabelle._
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
    12
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
    13
import java.lang.Class
56576
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
    14
import java.awt.event.MouseEvent
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
    15
import javax.swing.JMenuItem
56549
7cfc7aa121f3 added bad_words;
wenzelm
parents: 56547
diff changeset
    16
7cfc7aa121f3 added bad_words;
wenzelm
parents: 56547
diff changeset
    17
import scala.collection.mutable
56559
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
    18
import scala.swing.ComboBox
56561
5b6c3d69942a more elementary notion of "word" (similar to VoxSpell) -- treat hyphen as separator;
wenzelm
parents: 56559
diff changeset
    19
import scala.annotation.tailrec
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
    20
import scala.collection.immutable.SortedMap
56547
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
    21
56576
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
    22
import org.gjt.sp.jedit.jEdit
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
    23
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
56583
wenzelm
parents: 56581
diff changeset
    24
import org.gjt.sp.jedit.menu.EnhancedMenuItem
wenzelm
parents: 56581
diff changeset
    25
import org.gjt.sp.jedit.gui.DynamicContextMenuService
56574
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56573
diff changeset
    26
56547
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
    27
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
    28
object Spell_Checker
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
    29
{
56574
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56573
diff changeset
    30
  /* words within text */
56563
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    31
56565
wenzelm
parents: 56564
diff changeset
    32
  def marked_words(base: Text.Offset, text: String, mark: Text.Info[String] => Boolean)
wenzelm
parents: 56564
diff changeset
    33
    : List[Text.Info[String]] =
56563
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    34
  {
56564
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56563
diff changeset
    35
    val result = new mutable.ListBuffer[Text.Info[String]]
56563
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    36
    var offset = 0
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    37
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    38
    def apostrophe(c: Int): Boolean =
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    39
      c == '\'' && (offset + 1 == text.length || text(offset + 1) != '\'')
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    40
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    41
    @tailrec def scan(pred: Int => Boolean)
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    42
    {
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    43
      if (offset < text.length) {
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    44
        val c = text.codePointAt(offset)
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    45
        if (pred(c)) {
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    46
          offset += Character.charCount(c)
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    47
          scan(pred)
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    48
        }
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    49
      }
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    50
    }
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    51
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    52
    while (offset < text.length) {
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    53
      scan(c => !Character.isLetter(c))
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    54
      val start = offset
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    55
      scan(c => Character.isLetterOrDigit(c) || apostrophe(c))
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    56
      val stop = offset
56564
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56563
diff changeset
    57
      if (stop - start >= 2) {
56565
wenzelm
parents: 56564
diff changeset
    58
        val info = Text.Info(Text.Range(base + start, base + stop), text.substring(start, stop))
56564
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56563
diff changeset
    59
        if (mark(info)) result += info
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56563
diff changeset
    60
      }
56563
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    61
    }
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    62
    result.toList
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    63
  }
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    64
56576
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
    65
  def current_word(text_area: TextArea, rendering: Rendering, range: Text.Range)
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
    66
    : Option[Text.Info[String]] =
56574
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56573
diff changeset
    67
  {
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56573
diff changeset
    68
    for {
56576
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
    69
      spell_range <- rendering.spell_checker_point(range)
56574
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56573
diff changeset
    70
      text <- JEdit_Lib.try_get_text(text_area.getBuffer, spell_range)
56576
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
    71
      info <- marked_words(spell_range.start, text, info => info.range.overlaps(range)).headOption
56574
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56573
diff changeset
    72
    } yield info
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56573
diff changeset
    73
  }
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56573
diff changeset
    74
56563
9ac666f343d4 tuned signature;
wenzelm
parents: 56562
diff changeset
    75
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
    76
  /* dictionary declarations */
56570
282f3b06fa86 support for persistent user dictionaries;
wenzelm
parents: 56569
diff changeset
    77
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
    78
  class Dictionary private[Spell_Checker](val path: Path)
56557
18d921496aa5 updated to jortho-1.0-1: dictionaries from SCOWL 7.1, with parameters like aspell;
wenzelm
parents: 56552
diff changeset
    79
  {
18d921496aa5 updated to jortho-1.0-1: dictionaries from SCOWL 7.1, with parameters like aspell;
wenzelm
parents: 56552
diff changeset
    80
    val lang = path.split_ext._1.base.implode
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
    81
    val user_path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang)
56557
18d921496aa5 updated to jortho-1.0-1: dictionaries from SCOWL 7.1, with parameters like aspell;
wenzelm
parents: 56552
diff changeset
    82
    override def toString: String = lang
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
    83
  }
56570
282f3b06fa86 support for persistent user dictionaries;
wenzelm
parents: 56569
diff changeset
    84
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
    85
  private object Decl
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
    86
  {
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
    87
    def apply(name: String, include: Boolean): String =
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
    88
      if (include) name else "-" + name
56570
282f3b06fa86 support for persistent user dictionaries;
wenzelm
parents: 56569
diff changeset
    89
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
    90
    def unapply(decl: String): Option[(String, Boolean)] =
56570
282f3b06fa86 support for persistent user dictionaries;
wenzelm
parents: 56569
diff changeset
    91
    {
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
    92
      val decl1 = decl.trim
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
    93
      if (decl1 == "" || decl1.startsWith("#")) None
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
    94
      else
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
    95
        Library.try_unprefix("-", decl1.trim) match {
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
    96
          case None => Some((decl1, true))
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
    97
          case Some(decl2) => Some((decl2, false))
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
    98
        }
56570
282f3b06fa86 support for persistent user dictionaries;
wenzelm
parents: 56569
diff changeset
    99
    }
56557
18d921496aa5 updated to jortho-1.0-1: dictionaries from SCOWL 7.1, with parameters like aspell;
wenzelm
parents: 56552
diff changeset
   100
  }
56547
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   101
56559
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   102
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   103
  /* known dictionaries */
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   104
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   105
  def dictionaries(): List[Dictionary] =
56557
18d921496aa5 updated to jortho-1.0-1: dictionaries from SCOWL 7.1, with parameters like aspell;
wenzelm
parents: 56552
diff changeset
   106
    for {
18d921496aa5 updated to jortho-1.0-1: dictionaries from SCOWL 7.1, with parameters like aspell;
wenzelm
parents: 56552
diff changeset
   107
      path <- Path.split(Isabelle_System.getenv("JORTHO_DICTIONARIES"))
18d921496aa5 updated to jortho-1.0-1: dictionaries from SCOWL 7.1, with parameters like aspell;
wenzelm
parents: 56552
diff changeset
   108
      if path.is_file
18d921496aa5 updated to jortho-1.0-1: dictionaries from SCOWL 7.1, with parameters like aspell;
wenzelm
parents: 56552
diff changeset
   109
    } yield new Dictionary(path)
18d921496aa5 updated to jortho-1.0-1: dictionaries from SCOWL 7.1, with parameters like aspell;
wenzelm
parents: 56552
diff changeset
   110
56559
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   111
  def dictionaries_selector(): Option_Component =
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   112
  {
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   113
    Swing_Thread.require()
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   114
56569
wenzelm
parents: 56568
diff changeset
   115
    val option_name = "spell_checker_dictionary"
56559
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   116
    val opt = PIDE.options.value.check_name(option_name)
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   117
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   118
    val entries = dictionaries()
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   119
    val component = new ComboBox(entries) with Option_Component {
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   120
      name = option_name
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   121
      val title = opt.title()
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   122
      def load: Unit =
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   123
      {
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   124
        val lang = PIDE.options.string(option_name)
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   125
        entries.find(_.lang == lang) match {
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   126
          case Some(entry) => selection.item = entry
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   127
          case None =>
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   128
        }
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   129
      }
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   130
      def save: Unit = PIDE.options.string(option_name) = selection.item.lang
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   131
    }
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   132
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   133
    component.load()
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   134
    component.tooltip = opt.print_default
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   135
    component
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   136
  }
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   137
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   138
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   139
  /* create spell checker */
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   140
56564
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56563
diff changeset
   141
  def apply(dictionary: Dictionary): Spell_Checker = new Spell_Checker(dictionary)
56577
wenzelm
parents: 56576
diff changeset
   142
wenzelm
parents: 56576
diff changeset
   143
  private sealed case class Update(include: Boolean, permanent: Boolean)
56547
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   144
}
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   145
56559
eece73c31e38 added dictionaries_selector GUI;
wenzelm
parents: 56558
diff changeset
   146
56564
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56563
diff changeset
   147
class Spell_Checker private(dictionary: Spell_Checker.Dictionary)
56547
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   148
{
56564
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56563
diff changeset
   149
  override def toString: String = dictionary.toString
56547
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   150
56570
282f3b06fa86 support for persistent user dictionaries;
wenzelm
parents: 56569
diff changeset
   151
  private var dict = new Object
56577
wenzelm
parents: 56576
diff changeset
   152
  private var updates = SortedMap.empty[String, Spell_Checker.Update]
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   153
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   154
  private def included_iterator(): Iterator[String] =
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   155
    for {
56577
wenzelm
parents: 56576
diff changeset
   156
      (word, upd) <- updates.iterator
wenzelm
parents: 56576
diff changeset
   157
      if upd.include
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   158
    } yield word
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   159
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   160
  private def excluded(word: String): Boolean =
56577
wenzelm
parents: 56576
diff changeset
   161
    updates.get(word) match {
wenzelm
parents: 56576
diff changeset
   162
      case Some(upd) => !upd.include
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   163
      case None => false
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   164
    }
56570
282f3b06fa86 support for persistent user dictionaries;
wenzelm
parents: 56569
diff changeset
   165
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   166
  private def load()
56547
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   167
  {
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   168
    val main_dictionary = split_lines(File.read_gzip(dictionary.path))
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   169
56577
wenzelm
parents: 56576
diff changeset
   170
    val permanent_updates =
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   171
      if (dictionary.user_path.is_file)
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   172
        for {
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   173
          Spell_Checker.Decl(word, include) <- split_lines(File.read(dictionary.user_path))
56577
wenzelm
parents: 56576
diff changeset
   174
        } yield (word, Spell_Checker.Update(include, true))
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   175
      else Nil
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   176
56577
wenzelm
parents: 56576
diff changeset
   177
    updates =
wenzelm
parents: 56576
diff changeset
   178
      updates -- (for ((name, upd) <- updates.iterator; if upd.permanent) yield name) ++
wenzelm
parents: 56576
diff changeset
   179
        permanent_updates
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   180
56547
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   181
    val factory_class = Class.forName("com.inet.jortho.DictionaryFactory")
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   182
    val factory_cons = factory_class.getConstructor()
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   183
    factory_cons.setAccessible(true)
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   184
    val factory = factory_cons.newInstance()
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   185
56557
18d921496aa5 updated to jortho-1.0-1: dictionaries from SCOWL 7.1, with parameters like aspell;
wenzelm
parents: 56552
diff changeset
   186
    val add = factory_class.getDeclaredMethod("add", classOf[String])
18d921496aa5 updated to jortho-1.0-1: dictionaries from SCOWL 7.1, with parameters like aspell;
wenzelm
parents: 56552
diff changeset
   187
    add.setAccessible(true)
56570
282f3b06fa86 support for persistent user dictionaries;
wenzelm
parents: 56569
diff changeset
   188
282f3b06fa86 support for persistent user dictionaries;
wenzelm
parents: 56569
diff changeset
   189
    for {
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   190
      word <- main_dictionary.iterator ++ included_iterator()
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   191
      if !excluded(word)
56570
282f3b06fa86 support for persistent user dictionaries;
wenzelm
parents: 56569
diff changeset
   192
    } add.invoke(factory, word)
56547
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   193
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   194
    val create = factory_class.getDeclaredMethod("create")
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   195
    create.setAccessible(true)
56570
282f3b06fa86 support for persistent user dictionaries;
wenzelm
parents: 56569
diff changeset
   196
    dict = create.invoke(factory)
282f3b06fa86 support for persistent user dictionaries;
wenzelm
parents: 56569
diff changeset
   197
  }
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   198
  load()
56570
282f3b06fa86 support for persistent user dictionaries;
wenzelm
parents: 56569
diff changeset
   199
56574
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56573
diff changeset
   200
  private def save()
56570
282f3b06fa86 support for persistent user dictionaries;
wenzelm
parents: 56569
diff changeset
   201
  {
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   202
    val permanent_decls =
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   203
      (for {
56577
wenzelm
parents: 56576
diff changeset
   204
        (word, upd) <- updates.iterator
wenzelm
parents: 56576
diff changeset
   205
        if upd.permanent
wenzelm
parents: 56576
diff changeset
   206
      } yield Spell_Checker.Decl(word, upd.include)).toList
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   207
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   208
    if (!permanent_decls.isEmpty || dictionary.user_path.is_file) {
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   209
      val header =
56577
wenzelm
parents: 56576
diff changeset
   210
        "# Permanent updates for spell-checker dictionary " + quote(dictionary.lang) +
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   211
"""
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   212
#
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   213
#   * each line contains at most one word
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   214
#   * extra blanks are ignored
56574
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56573
diff changeset
   215
#   * lines starting with "#" are stripped
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   216
#   * lines starting with "-" indicate excluded words
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   217
#
56574
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56573
diff changeset
   218
#:mode=text:encoding=UTF-8:
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56573
diff changeset
   219
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   220
"""
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   221
      Isabelle_System.mkdirs(dictionary.user_path.expand.dir)
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   222
      File.write(dictionary.user_path, header + cat_lines(permanent_decls))
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   223
    }
56547
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   224
  }
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   225
56574
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56573
diff changeset
   226
  def update(word: String, include: Boolean, permanent: Boolean)
56547
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   227
  {
56577
wenzelm
parents: 56576
diff changeset
   228
    updates += (word -> Spell_Checker.Update(include, permanent))
56574
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56573
diff changeset
   229
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56573
diff changeset
   230
    if (include) {
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56573
diff changeset
   231
      if (permanent) save()
56570
282f3b06fa86 support for persistent user dictionaries;
wenzelm
parents: 56569
diff changeset
   232
56574
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56573
diff changeset
   233
      val m = dict.getClass.getDeclaredMethod("add", classOf[String])
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56573
diff changeset
   234
      m.setAccessible(true)
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56573
diff changeset
   235
      m.invoke(dict, word)
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56573
diff changeset
   236
    }
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56573
diff changeset
   237
    else { save(); load() }
56570
282f3b06fa86 support for persistent user dictionaries;
wenzelm
parents: 56569
diff changeset
   238
  }
282f3b06fa86 support for persistent user dictionaries;
wenzelm
parents: 56569
diff changeset
   239
56574
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56573
diff changeset
   240
  def reset()
56570
282f3b06fa86 support for persistent user dictionaries;
wenzelm
parents: 56569
diff changeset
   241
  {
56577
wenzelm
parents: 56576
diff changeset
   242
    updates = SortedMap.empty
56573
0f9d2e13187e more explicit user declarations for main dictionary;
wenzelm
parents: 56570
diff changeset
   243
    load()
56547
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   244
  }
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   245
56552
76cf86240cb7 some case-mangling;
wenzelm
parents: 56549
diff changeset
   246
  def contains(word: String): Boolean =
56547
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   247
  {
56564
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56563
diff changeset
   248
    val m = dict.getClass.getSuperclass.getDeclaredMethod("exist", classOf[String])
56547
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   249
    m.setAccessible(true)
56564
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56563
diff changeset
   250
    m.invoke(dict, word).asInstanceOf[java.lang.Boolean].booleanValue
56547
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   251
  }
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   252
56552
76cf86240cb7 some case-mangling;
wenzelm
parents: 56549
diff changeset
   253
  def check(word: String): Boolean =
76cf86240cb7 some case-mangling;
wenzelm
parents: 56549
diff changeset
   254
    contains(word) ||
56568
6e4f2d4215b0 eliminated somewhat pointless locale parameter;
wenzelm
parents: 56567
diff changeset
   255
    Library.is_all_caps(word) && contains(Library.lowercase(word)) ||
56552
76cf86240cb7 some case-mangling;
wenzelm
parents: 56549
diff changeset
   256
    Library.is_capitalized(word) &&
56568
6e4f2d4215b0 eliminated somewhat pointless locale parameter;
wenzelm
parents: 56567
diff changeset
   257
      (contains(Library.lowercase(word)) || contains(Library.uppercase(word)))
56552
76cf86240cb7 some case-mangling;
wenzelm
parents: 56549
diff changeset
   258
56547
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   259
  def complete(word: String): List[String] =
56566
46a4c6b688c9 clarified complete: participate in case-mangling of check;
wenzelm
parents: 56565
diff changeset
   260
    if (check(word)) Nil
46a4c6b688c9 clarified complete: participate in case-mangling of check;
wenzelm
parents: 56565
diff changeset
   261
    else {
46a4c6b688c9 clarified complete: participate in case-mangling of check;
wenzelm
parents: 56565
diff changeset
   262
      val m = dict.getClass.getSuperclass. getDeclaredMethod("searchSuggestions", classOf[String])
46a4c6b688c9 clarified complete: participate in case-mangling of check;
wenzelm
parents: 56565
diff changeset
   263
      m.setAccessible(true)
46a4c6b688c9 clarified complete: participate in case-mangling of check;
wenzelm
parents: 56565
diff changeset
   264
      m.invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
46a4c6b688c9 clarified complete: participate in case-mangling of check;
wenzelm
parents: 56565
diff changeset
   265
    }
56549
7cfc7aa121f3 added bad_words;
wenzelm
parents: 56547
diff changeset
   266
56565
wenzelm
parents: 56564
diff changeset
   267
  def marked_words(base: Text.Offset, text: String): List[Text.Info[String]] =
wenzelm
parents: 56564
diff changeset
   268
    Spell_Checker.marked_words(base, text, info => !check(info.info))
56547
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   269
}
e9bb73d7b6cf added spell-checker based on jortho-1.0;
wenzelm
parents:
diff changeset
   270
56558
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   271
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   272
class Spell_Checker_Variable
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   273
{
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   274
  private val no_spell_checker: (String, Option[Spell_Checker]) = ("", None)
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   275
  private var current_spell_checker = no_spell_checker
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   276
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   277
  def get: Option[Spell_Checker] = synchronized { current_spell_checker._2 }
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   278
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   279
  def update(options: Options): Unit = synchronized {
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   280
    if (options.bool("spell_checker")) {
56569
wenzelm
parents: 56568
diff changeset
   281
      val lang = options.string("spell_checker_dictionary")
56558
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   282
      if (current_spell_checker._1 != lang) {
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   283
        Spell_Checker.dictionaries.find(_.lang == lang) match {
56564
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56563
diff changeset
   284
          case Some(dictionary) =>
56558
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   285
            val spell_checker =
56564
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56563
diff changeset
   286
              Exn.capture { Spell_Checker(dictionary) } match {
56558
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   287
                case Exn.Res(spell_checker) => Some(spell_checker)
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   288
                case Exn.Exn(_) => None
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   289
              }
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   290
            current_spell_checker = (lang, spell_checker)
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   291
          case None =>
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   292
            current_spell_checker = no_spell_checker
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   293
        }
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   294
      }
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   295
    }
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   296
    else current_spell_checker = no_spell_checker
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   297
  }
05c833d402bc tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents: 56557
diff changeset
   298
}
56576
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   299
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   300
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   301
class Spell_Checker_Menu extends DynamicContextMenuService
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   302
{
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   303
  def createMenu(text_area: JEditTextArea, evt: MouseEvent): Array[JMenuItem] =
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   304
  {
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   305
    if (evt != null && evt.getSource == text_area.getPainter) {
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   306
      val result =
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   307
        for {
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   308
          spell_checker <- PIDE.spell_checker.get
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   309
          doc_view <- PIDE.document_view(text_area)
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   310
          rendering = doc_view.get_rendering()
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   311
          offset = text_area.xyToOffset(evt.getX, evt.getY)
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   312
          if offset >= 0
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   313
          range = JEdit_Lib.point_range(text_area.getBuffer, offset)
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   314
          Text.Info(_, word) <- Spell_Checker.current_word(text_area, rendering, range)
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   315
        } yield spell_checker.check(word)
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   316
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   317
      result match {
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   318
        case Some(known_word) =>
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   319
          val context = jEdit.getActionContext()
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   320
          def item(action: String) =
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   321
            new EnhancedMenuItem(context.getAction(action).getLabel, action, context)
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   322
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   323
          if (known_word)
56581
af3e6576e680 tuned menu;
wenzelm
parents: 56577
diff changeset
   324
            Array(
af3e6576e680 tuned menu;
wenzelm
parents: 56577
diff changeset
   325
              item("isabelle.exclude-word"),
af3e6576e680 tuned menu;
wenzelm
parents: 56577
diff changeset
   326
              item("isabelle.exclude-word-permanently"),
af3e6576e680 tuned menu;
wenzelm
parents: 56577
diff changeset
   327
              item("isabelle.reset-words"))
56576
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   328
          else
56581
af3e6576e680 tuned menu;
wenzelm
parents: 56577
diff changeset
   329
            Array(
af3e6576e680 tuned menu;
wenzelm
parents: 56577
diff changeset
   330
              item("isabelle.include-word"),
af3e6576e680 tuned menu;
wenzelm
parents: 56577
diff changeset
   331
              item("isabelle.include-word-permanently"),
af3e6576e680 tuned menu;
wenzelm
parents: 56577
diff changeset
   332
              item("isabelle.reset-words"))
56576
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   333
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   334
        case None => null
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   335
      }
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   336
    }
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   337
    else null
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   338
  }
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56574
diff changeset
   339
}