author | wenzelm |
Sun, 01 Mar 2020 22:05:47 +0100 | |
changeset 71500 | a3ed1b0a132f |
parent 66137 | d2923067b376 |
child 73337 | 0af9e7e4476f |
permissions | -rw-r--r-- |
65139 | 1 |
/* Title: Tools/jEdit/src/jedit_spell_checker.scala |
56547 | 2 |
Author: Makarius |
3 |
||
65139 | 4 |
Specific spell-checker support for Isabelle/jEdit. |
56547 | 5 |
*/ |
6 |
||
7 |
package isabelle.jedit |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
58549 | 12 |
import javax.swing.JMenuItem |
56559 | 13 |
import scala.swing.ComboBox |
56547 | 14 |
|
58549 | 15 |
import org.gjt.sp.jedit.menu.EnhancedMenuItem |
65139 | 16 |
import org.gjt.sp.jedit.jEdit |
58549 | 17 |
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} |
56574
2b38472a4695
some actions to maintain spell-checker dictionary;
wenzelm
parents:
56573
diff
changeset
|
18 |
|
56547 | 19 |
|
65139 | 20 |
object JEdit_Spell_Checker |
56547 | 21 |
{ |
65139 | 22 |
/* completion */ |
58549 | 23 |
|
66119 | 24 |
def completion( |
25 |
rendering: JEdit_Rendering, explicit: Boolean, caret: Text.Offset): Option[Completion.Result] = |
|
58549 | 26 |
{ |
66119 | 27 |
PIDE.plugin.spell_checker.get match { |
28 |
case Some(spell_checker) if explicit => |
|
29 |
spell_checker.completion(rendering, caret) |
|
30 |
case _ => None |
|
31 |
} |
|
58549 | 32 |
} |
33 |
||
34 |
||
65139 | 35 |
/* context menu */ |
58549 | 36 |
|
37 |
def context_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] = |
|
38 |
{ |
|
39 |
val result = |
|
40 |
for { |
|
65239
509a9b0ad02e
avoid global variables with implicit initialization;
wenzelm
parents:
65139
diff
changeset
|
41 |
spell_checker <- PIDE.plugin.spell_checker.get |
64882 | 42 |
doc_view <- Document_View.get(text_area) |
58549 | 43 |
rendering = doc_view.get_rendering() |
44 |
range = JEdit_Lib.point_range(text_area.getBuffer, offset) |
|
66116 | 45 |
Text.Info(_, word) <- Spell_Checker.current_word(rendering, range) |
58549 | 46 |
} yield (spell_checker, word) |
47 |
||
48 |
result match { |
|
49 |
case Some((spell_checker, word)) => |
|
50 |
||
51 |
val context = jEdit.getActionContext() |
|
52 |
def item(name: String): JMenuItem = |
|
53 |
new EnhancedMenuItem(context.getAction(name).getLabel, name, context) |
|
54 |
||
55 |
val complete_items = |
|
66137 | 56 |
if (spell_checker.complete(word).nonEmpty) List(item("isabelle.complete-word")) |
58549 | 57 |
else Nil |
58 |
||
59 |
val update_items = |
|
60 |
if (spell_checker.check(word)) |
|
61 |
List(item("isabelle.exclude-word"), item("isabelle.exclude-word-permanently")) |
|
62 |
else |
|
63 |
List(item("isabelle.include-word"), item("isabelle.include-word-permanently")) |
|
64 |
||
65 |
val reset_items = |
|
66 |
spell_checker.reset_enabled() match { |
|
67 |
case 0 => Nil |
|
68 |
case n => |
|
69 |
val name = "isabelle.reset-words" |
|
70 |
val label = context.getAction(name).getLabel |
|
71 |
List(new EnhancedMenuItem(label + " (" + n + ")", name, context)) |
|
72 |
} |
|
73 |
||
74 |
complete_items ::: update_items ::: reset_items |
|
75 |
||
76 |
case None => Nil |
|
77 |
} |
|
78 |
} |
|
79 |
||
80 |
||
65139 | 81 |
/* dictionaries */ |
56557
18d921496aa5
updated to jortho-1.0-1: dictionaries from SCOWL 7.1, with parameters like aspell;
wenzelm
parents:
56552
diff
changeset
|
82 |
|
56559 | 83 |
def dictionaries_selector(): Option_Component = |
84 |
{ |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56662
diff
changeset
|
85 |
GUI_Thread.require {} |
56559 | 86 |
|
56569 | 87 |
val option_name = "spell_checker_dictionary" |
56559 | 88 |
val opt = PIDE.options.value.check_name(option_name) |
89 |
||
65139 | 90 |
val entries = Spell_Checker.dictionaries() |
56559 | 91 |
val component = new ComboBox(entries) with Option_Component { |
92 |
name = option_name |
|
93 |
val title = opt.title() |
|
94 |
def load: Unit = |
|
95 |
{ |
|
96 |
val lang = PIDE.options.string(option_name) |
|
97 |
entries.find(_.lang == lang) match { |
|
98 |
case Some(entry) => selection.item = entry |
|
99 |
case None => |
|
100 |
} |
|
101 |
} |
|
102 |
def save: Unit = PIDE.options.string(option_name) = selection.item.lang |
|
103 |
} |
|
104 |
||
105 |
component.load() |
|
56622
891d1b8b64fb
clarified tooltip_lines: HTML.encode already takes care of newline (but not space);
wenzelm
parents:
56611
diff
changeset
|
106 |
component.tooltip = GUI.tooltip_lines(opt.print_default) |
56559 | 107 |
component |
108 |
} |
|
56547 | 109 |
} |