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