1 /* Title: Tools/jEdit/src/spell_checker.scala |
|
2 Author: Makarius |
|
3 |
|
4 Spell checker with completion, based on JOrtho (see |
|
5 http://sourceforge.net/projects/jortho). |
|
6 */ |
|
7 |
|
8 package isabelle.jedit |
|
9 |
|
10 |
|
11 import isabelle._ |
|
12 |
|
13 import java.lang.Class |
|
14 |
|
15 import javax.swing.JMenuItem |
|
16 |
|
17 import scala.collection.mutable |
|
18 import scala.swing.ComboBox |
|
19 import scala.annotation.tailrec |
|
20 import scala.collection.immutable.SortedMap |
|
21 |
|
22 import org.gjt.sp.jedit.menu.EnhancedMenuItem |
|
23 import org.gjt.sp.jedit.{jEdit, Buffer} |
|
24 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} |
|
25 |
|
26 |
|
27 object Spell_Checker |
|
28 { |
|
29 /** words within text **/ |
|
30 |
|
31 def marked_words(base: Text.Offset, text: String, mark: Text.Info[String] => Boolean) |
|
32 : List[Text.Info[String]] = |
|
33 { |
|
34 val result = new mutable.ListBuffer[Text.Info[String]] |
|
35 var offset = 0 |
|
36 |
|
37 def apostrophe(c: Int): Boolean = |
|
38 c == '\'' && (offset + 1 == text.length || text(offset + 1) != '\'') |
|
39 |
|
40 @tailrec def scan(pred: Int => Boolean) |
|
41 { |
|
42 if (offset < text.length) { |
|
43 val c = text.codePointAt(offset) |
|
44 if (pred(c)) { |
|
45 offset += Character.charCount(c) |
|
46 scan(pred) |
|
47 } |
|
48 } |
|
49 } |
|
50 |
|
51 while (offset < text.length) { |
|
52 scan(c => !Character.isLetter(c)) |
|
53 val start = offset |
|
54 scan(c => Character.isLetterOrDigit(c) || apostrophe(c)) |
|
55 val stop = offset |
|
56 if (stop - start >= 2) { |
|
57 val info = Text.Info(Text.Range(base + start, base + stop), text.substring(start, stop)) |
|
58 if (mark(info)) result += info |
|
59 } |
|
60 } |
|
61 result.toList |
|
62 } |
|
63 |
|
64 def current_word(text_area: TextArea, rendering: JEdit_Rendering, range: Text.Range) |
|
65 : Option[Text.Info[String]] = |
|
66 { |
|
67 for { |
|
68 spell_range <- rendering.spell_checker_point(range) |
|
69 text <- JEdit_Lib.try_get_text(text_area.getBuffer, spell_range) |
|
70 info <- marked_words(spell_range.start, text, info => info.range.overlaps(range)).headOption |
|
71 } yield info |
|
72 } |
|
73 |
|
74 |
|
75 |
|
76 /** completion **/ |
|
77 |
|
78 def completion(text_area: TextArea, explicit: Boolean, rendering: JEdit_Rendering) |
|
79 : Option[Completion.Result] = |
|
80 { |
|
81 for { |
|
82 spell_checker <- PIDE.spell_checker.get |
|
83 if explicit |
|
84 range = JEdit_Lib.before_caret_range(text_area, rendering) |
|
85 word <- current_word(text_area, rendering, range) |
|
86 words = spell_checker.complete(word.info) |
|
87 if words.nonEmpty |
|
88 descr = "(from dictionary " + quote(spell_checker.toString) + ")" |
|
89 items = |
|
90 words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false)) |
|
91 } yield Completion.Result(word.range, word.info, false, items) |
|
92 } |
|
93 |
|
94 |
|
95 |
|
96 /** context menu **/ |
|
97 |
|
98 def context_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] = |
|
99 { |
|
100 val result = |
|
101 for { |
|
102 spell_checker <- PIDE.spell_checker.get |
|
103 doc_view <- Document_View.get(text_area) |
|
104 rendering = doc_view.get_rendering() |
|
105 range = JEdit_Lib.point_range(text_area.getBuffer, offset) |
|
106 Text.Info(_, word) <- current_word(text_area, rendering, range) |
|
107 } yield (spell_checker, word) |
|
108 |
|
109 result match { |
|
110 case Some((spell_checker, word)) => |
|
111 |
|
112 val context = jEdit.getActionContext() |
|
113 def item(name: String): JMenuItem = |
|
114 new EnhancedMenuItem(context.getAction(name).getLabel, name, context) |
|
115 |
|
116 val complete_items = |
|
117 if (spell_checker.complete_enabled(word)) List(item("isabelle.complete-word")) |
|
118 else Nil |
|
119 |
|
120 val update_items = |
|
121 if (spell_checker.check(word)) |
|
122 List(item("isabelle.exclude-word"), item("isabelle.exclude-word-permanently")) |
|
123 else |
|
124 List(item("isabelle.include-word"), item("isabelle.include-word-permanently")) |
|
125 |
|
126 val reset_items = |
|
127 spell_checker.reset_enabled() match { |
|
128 case 0 => Nil |
|
129 case n => |
|
130 val name = "isabelle.reset-words" |
|
131 val label = context.getAction(name).getLabel |
|
132 List(new EnhancedMenuItem(label + " (" + n + ")", name, context)) |
|
133 } |
|
134 |
|
135 complete_items ::: update_items ::: reset_items |
|
136 |
|
137 case None => Nil |
|
138 } |
|
139 } |
|
140 |
|
141 |
|
142 |
|
143 /** dictionary **/ |
|
144 |
|
145 /* declarations */ |
|
146 |
|
147 class Dictionary private[Spell_Checker](val path: Path) |
|
148 { |
|
149 val lang = path.split_ext._1.base.implode |
|
150 val user_path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang) |
|
151 override def toString: String = lang |
|
152 } |
|
153 |
|
154 private object Decl |
|
155 { |
|
156 def apply(name: String, include: Boolean): String = |
|
157 if (include) name else "-" + name |
|
158 |
|
159 def unapply(decl: String): Option[(String, Boolean)] = |
|
160 { |
|
161 val decl1 = decl.trim |
|
162 if (decl1 == "" || decl1.startsWith("#")) None |
|
163 else |
|
164 Library.try_unprefix("-", decl1.trim) match { |
|
165 case None => Some((decl1, true)) |
|
166 case Some(decl2) => Some((decl2, false)) |
|
167 } |
|
168 } |
|
169 } |
|
170 |
|
171 |
|
172 /* known dictionaries */ |
|
173 |
|
174 def dictionaries(): List[Dictionary] = |
|
175 for { |
|
176 path <- Path.split(Isabelle_System.getenv("JORTHO_DICTIONARIES")) |
|
177 if path.is_file |
|
178 } yield new Dictionary(path) |
|
179 |
|
180 def dictionaries_selector(): Option_Component = |
|
181 { |
|
182 GUI_Thread.require {} |
|
183 |
|
184 val option_name = "spell_checker_dictionary" |
|
185 val opt = PIDE.options.value.check_name(option_name) |
|
186 |
|
187 val entries = dictionaries() |
|
188 val component = new ComboBox(entries) with Option_Component { |
|
189 name = option_name |
|
190 val title = opt.title() |
|
191 def load: Unit = |
|
192 { |
|
193 val lang = PIDE.options.string(option_name) |
|
194 entries.find(_.lang == lang) match { |
|
195 case Some(entry) => selection.item = entry |
|
196 case None => |
|
197 } |
|
198 } |
|
199 def save: Unit = PIDE.options.string(option_name) = selection.item.lang |
|
200 } |
|
201 |
|
202 component.load() |
|
203 component.tooltip = GUI.tooltip_lines(opt.print_default) |
|
204 component |
|
205 } |
|
206 |
|
207 |
|
208 /* create spell checker */ |
|
209 |
|
210 def apply(dictionary: Dictionary): Spell_Checker = new Spell_Checker(dictionary) |
|
211 |
|
212 private sealed case class Update(include: Boolean, permanent: Boolean) |
|
213 } |
|
214 |
|
215 |
|
216 class Spell_Checker private(dictionary: Spell_Checker.Dictionary) |
|
217 { |
|
218 override def toString: String = dictionary.toString |
|
219 |
|
220 |
|
221 /* main dictionary content */ |
|
222 |
|
223 private var dict = new Object |
|
224 private var updates = SortedMap.empty[String, Spell_Checker.Update] |
|
225 |
|
226 private def included_iterator(): Iterator[String] = |
|
227 for { |
|
228 (word, upd) <- updates.iterator |
|
229 if upd.include |
|
230 } yield word |
|
231 |
|
232 private def excluded(word: String): Boolean = |
|
233 updates.get(word) match { |
|
234 case Some(upd) => !upd.include |
|
235 case None => false |
|
236 } |
|
237 |
|
238 private def load() |
|
239 { |
|
240 val main_dictionary = split_lines(File.read_gzip(dictionary.path)) |
|
241 |
|
242 val permanent_updates = |
|
243 if (dictionary.user_path.is_file) |
|
244 for { |
|
245 Spell_Checker.Decl(word, include) <- split_lines(File.read(dictionary.user_path)) |
|
246 } yield (word, Spell_Checker.Update(include, true)) |
|
247 else Nil |
|
248 |
|
249 updates = |
|
250 updates -- (for ((name, upd) <- updates.iterator; if upd.permanent) yield name) ++ |
|
251 permanent_updates |
|
252 |
|
253 val factory_class = Class.forName("com.inet.jortho.DictionaryFactory") |
|
254 val factory_cons = factory_class.getConstructor() |
|
255 factory_cons.setAccessible(true) |
|
256 val factory = factory_cons.newInstance() |
|
257 |
|
258 val add = Untyped.method(factory_class, "add", classOf[String]) |
|
259 |
|
260 for { |
|
261 word <- main_dictionary.iterator ++ included_iterator() |
|
262 if !excluded(word) |
|
263 } add.invoke(factory, word) |
|
264 |
|
265 dict = Untyped.method(factory_class, "create").invoke(factory) |
|
266 } |
|
267 load() |
|
268 |
|
269 private def save() |
|
270 { |
|
271 val permanent_decls = |
|
272 (for { |
|
273 (word, upd) <- updates.iterator |
|
274 if upd.permanent |
|
275 } yield Spell_Checker.Decl(word, upd.include)).toList |
|
276 |
|
277 if (permanent_decls.nonEmpty || dictionary.user_path.is_file) { |
|
278 val header = """# User updates for spell-checker dictionary |
|
279 # |
|
280 # * each line contains at most one word |
|
281 # * extra blanks are ignored |
|
282 # * lines starting with "#" are stripped |
|
283 # * lines starting with "-" indicate excluded words |
|
284 # |
|
285 #:mode=text:encoding=UTF-8: |
|
286 |
|
287 """ |
|
288 Isabelle_System.mkdirs(dictionary.user_path.expand.dir) |
|
289 File.write(dictionary.user_path, header + cat_lines(permanent_decls)) |
|
290 } |
|
291 } |
|
292 |
|
293 def update(word: String, include: Boolean, permanent: Boolean) |
|
294 { |
|
295 updates += (word -> Spell_Checker.Update(include, permanent)) |
|
296 |
|
297 if (include) { |
|
298 if (permanent) save() |
|
299 Untyped.method(dict.getClass, "add", classOf[String]).invoke(dict, word) |
|
300 } |
|
301 else { save(); load() } |
|
302 } |
|
303 |
|
304 def reset() |
|
305 { |
|
306 updates = SortedMap.empty |
|
307 load() |
|
308 } |
|
309 |
|
310 def reset_enabled(): Int = |
|
311 updates.valuesIterator.filter(upd => !upd.permanent).length |
|
312 |
|
313 |
|
314 /* check known words */ |
|
315 |
|
316 def contains(word: String): Boolean = |
|
317 Untyped.method(dict.getClass.getSuperclass, "exist", classOf[String]). |
|
318 invoke(dict, word).asInstanceOf[java.lang.Boolean].booleanValue |
|
319 |
|
320 def check(word: String): Boolean = |
|
321 word match { |
|
322 case Word.Case(c) if c != Word.Lowercase => |
|
323 contains(word) || contains(Word.lowercase(word)) |
|
324 case _ => |
|
325 contains(word) |
|
326 } |
|
327 |
|
328 def marked_words(base: Text.Offset, text: String): List[Text.Info[String]] = |
|
329 Spell_Checker.marked_words(base, text, info => !check(info.info)) |
|
330 |
|
331 |
|
332 /* suggestions for unknown words */ |
|
333 |
|
334 private def suggestions(word: String): Option[List[String]] = |
|
335 { |
|
336 val res = |
|
337 Untyped.method(dict.getClass.getSuperclass, "searchSuggestions", classOf[String]). |
|
338 invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString) |
|
339 if (res.isEmpty) None else Some(res) |
|
340 } |
|
341 |
|
342 def complete(word: String): List[String] = |
|
343 if (check(word)) Nil |
|
344 else { |
|
345 val word_case = Word.Case.unapply(word) |
|
346 def recover_case(s: String) = |
|
347 word_case match { |
|
348 case Some(c) => Word.Case(c, s) |
|
349 case None => s |
|
350 } |
|
351 val result = |
|
352 word_case match { |
|
353 case Some(c) if c != Word.Lowercase => |
|
354 suggestions(word) orElse suggestions(Word.lowercase(word)) |
|
355 case _ => |
|
356 suggestions(word) |
|
357 } |
|
358 result.getOrElse(Nil).map(recover_case) |
|
359 } |
|
360 |
|
361 def complete_enabled(word: String): Boolean = complete(word).nonEmpty |
|
362 } |
|
363 |
|
364 |
|
365 class Spell_Checker_Variable |
|
366 { |
|
367 private val no_spell_checker: (String, Option[Spell_Checker]) = ("", None) |
|
368 private var current_spell_checker = no_spell_checker |
|
369 |
|
370 def get: Option[Spell_Checker] = synchronized { current_spell_checker._2 } |
|
371 |
|
372 def update(options: Options): Unit = synchronized { |
|
373 if (options.bool("spell_checker")) { |
|
374 val lang = options.string("spell_checker_dictionary") |
|
375 if (current_spell_checker._1 != lang) { |
|
376 Spell_Checker.dictionaries.find(_.lang == lang) match { |
|
377 case Some(dictionary) => |
|
378 val spell_checker = |
|
379 Exn.capture { Spell_Checker(dictionary) } match { |
|
380 case Exn.Res(spell_checker) => Some(spell_checker) |
|
381 case Exn.Exn(_) => None |
|
382 } |
|
383 current_spell_checker = (lang, spell_checker) |
|
384 case None => |
|
385 current_spell_checker = no_spell_checker |
|
386 } |
|
387 } |
|
388 } |
|
389 else current_spell_checker = no_spell_checker |
|
390 } |
|
391 } |
|
392 |
|