author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 72761 | 4519eeefe3b5 |
permissions | -rw-r--r-- |
66141 | 1 |
/* Title: Tools/VSCode/src/vscode_spell_checker.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Specific spell-checker support for Isabelle/VSCode. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle.vscode |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
12 |
||
75393 | 13 |
object VSCode_Spell_Checker { |
14 |
def decoration(rendering: VSCode_Rendering): VSCode_Model.Decoration = { |
|
66141 | 15 |
val model = rendering.model |
16 |
val ranges = |
|
17 |
(for { |
|
66143 | 18 |
spell_checker <- rendering.resources.spell_checker.get.iterator |
67395
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67014
diff
changeset
|
19 |
spell <- rendering.spell_checker(model.content.text_range).iterator |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67014
diff
changeset
|
20 |
text <- model.get_text(spell.range).iterator |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67014
diff
changeset
|
21 |
info <- spell_checker.marked_words(spell.range.start, text).iterator |
66141 | 22 |
} yield info.range).toList |
72761 | 23 |
VSCode_Model.Decoration.ranges("spell_checker", ranges) |
66141 | 24 |
} |
25 |
||
26 |
def completion(rendering: VSCode_Rendering, caret: Text.Offset): Option[Completion.Result] = |
|
66143 | 27 |
rendering.resources.spell_checker.get.flatMap(_.completion(rendering, caret)) |
66141 | 28 |
|
75393 | 29 |
def menu_items(rendering: VSCode_Rendering, caret: Text.Offset): List[LSP.CompletionItem] = { |
66141 | 30 |
val result = |
31 |
for { |
|
66143 | 32 |
spell_checker <- rendering.resources.spell_checker.get |
66141 | 33 |
range = rendering.before_caret_range(caret) |
34 |
Text.Info(_, word) <- Spell_Checker.current_word(rendering, range) |
|
35 |
} yield (spell_checker, word) |
|
36 |
||
37 |
result match { |
|
38 |
case Some((spell_checker, word)) => |
|
39 |
||
72761 | 40 |
def item(command: LSP.Command): LSP.CompletionItem = |
41 |
LSP.CompletionItem( |
|
66141 | 42 |
label = command.title, |
43 |
text = Some(""), |
|
66143 | 44 |
range = Some(rendering.model.content.doc.range(Text.Range(caret))), |
66141 | 45 |
command = Some(command)) |
46 |
||
47 |
val update_items = |
|
48 |
if (spell_checker.check(word)) |
|
49 |
List( |
|
72761 | 50 |
item(LSP.Exclude_Word.command), |
51 |
item(LSP.Exclude_Word_Permanently.command)) |
|
66141 | 52 |
else |
53 |
List( |
|
72761 | 54 |
item(LSP.Include_Word.command), |
55 |
item(LSP.Include_Word_Permanently.command)) |
|
66141 | 56 |
|
57 |
val reset_items = |
|
58 |
spell_checker.reset_enabled() match { |
|
59 |
case 0 => Nil |
|
60 |
case n => |
|
72761 | 61 |
val command = LSP.Reset_Words.command |
66141 | 62 |
List(item(command).copy(label = command.title + " (" + n + ")")) |
63 |
} |
|
64 |
||
65 |
update_items ::: reset_items |
|
66 |
||
67 |
case None => Nil |
|
68 |
} |
|
69 |
} |
|
70 |
} |