--- a/src/Pure/build-jars Tue Jun 20 16:17:54 2017 +0200
+++ b/src/Pure/build-jars Tue Jun 20 17:08:24 2017 +0200
@@ -174,6 +174,7 @@
../Tools/VSCode/src/state_panel.scala
../Tools/VSCode/src/vscode_rendering.scala
../Tools/VSCode/src/vscode_resources.scala
+ ../Tools/VSCode/src/vscode_spell_checker.scala
)
--- a/src/Tools/VSCode/src/vscode_rendering.scala Tue Jun 20 16:17:54 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Tue Jun 20 17:08:24 2017 +0200
@@ -100,7 +100,7 @@
val results =
Completion.Result.merge(history,
Completion.Result.merge(history, semantic_completion, syntax_completion),
- spell_checker_completion(caret))
+ VSCode_Spell_Checker.completion(rendering, caret))
results match {
case None => Nil
case Some(result) =>
@@ -109,7 +109,7 @@
label = item.replacement,
detail = Some(item.description.mkString(" ")),
range = Some(doc.range(item.range)))) :::
- spell_checker_menu(caret)
+ VSCode_Spell_Checker.menu_items(rendering, caret)
}
}
}
@@ -192,67 +192,6 @@
message_underline_color(VSCode_Rendering.dotted_elements, range)
- /* spell checker */
-
- def spell_checker: Document_Model.Decoration =
- {
- val ranges =
- (for {
- spell_checker <- model.resources.spell_checker.get.iterator
- spell_range <- spell_checker_ranges(model.content.text_range).iterator
- text <- model.try_get_text(spell_range).iterator
- info <- spell_checker.marked_words(spell_range.start, text).iterator
- } yield info.range).toList
- Document_Model.Decoration.ranges("spell_checker", ranges)
- }
-
- def spell_checker_completion(caret: Text.Offset): Option[Completion.Result] =
- model.resources.spell_checker.get.flatMap(_.completion(rendering, caret))
-
- def spell_checker_menu(caret: Text.Offset): List[Protocol.CompletionItem] =
- {
- val result =
- for {
- spell_checker <- model.resources.spell_checker.get
- range = before_caret_range(caret)
- Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
- } yield (spell_checker, word)
-
- result match {
- case Some((spell_checker, word)) =>
-
- def item(command: Protocol.Command): Protocol.CompletionItem =
- Protocol.CompletionItem(
- label = command.title,
- text = Some(""),
- range = Some(model.content.doc.range(Text.Range(caret))),
- command = Some(command))
-
- val update_items =
- if (spell_checker.check(word))
- List(
- item(Protocol.Exclude_Word.command),
- item(Protocol.Exclude_Word_Permanently.command))
- else
- List(
- item(Protocol.Include_Word.command),
- item(Protocol.Include_Word_Permanently.command))
-
- val reset_items =
- spell_checker.reset_enabled() match {
- case 0 => Nil
- case n =>
- val command = Protocol.Reset_Words.command
- List(item(command).copy(label = command.title + " (" + n + ")"))
- }
-
- update_items ::: reset_items
-
- case None => Nil
- }
- }
-
-
/* decorations */
def decorations: List[Document_Model.Decoration] = // list of canonical length and order
@@ -273,7 +212,7 @@
() =>
VSCode_Rendering.color_decorations("dotted_", VSCode_Rendering.dotted_colors,
dotted(model.content.text_range)))).flatten :::
- List(spell_checker)
+ List(VSCode_Spell_Checker.decoration(rendering))
def decoration_output(decoration: Document_Model.Decoration): Protocol.Decoration =
{
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/src/vscode_spell_checker.scala Tue Jun 20 17:08:24 2017 +0200
@@ -0,0 +1,74 @@
+/* Title: Tools/VSCode/src/vscode_spell_checker.scala
+ Author: Makarius
+
+Specific spell-checker support for Isabelle/VSCode.
+*/
+
+package isabelle.vscode
+
+
+import isabelle._
+
+
+object VSCode_Spell_Checker
+{
+ def decoration(rendering: VSCode_Rendering): Document_Model.Decoration =
+ {
+ val model = rendering.model
+ val ranges =
+ (for {
+ spell_checker <- model.resources.spell_checker.get.iterator
+ spell_range <- rendering.spell_checker_ranges(model.content.text_range).iterator
+ text <- model.try_get_text(spell_range).iterator
+ info <- spell_checker.marked_words(spell_range.start, text).iterator
+ } yield info.range).toList
+ Document_Model.Decoration.ranges("spell_checker", ranges)
+ }
+
+ def completion(rendering: VSCode_Rendering, caret: Text.Offset): Option[Completion.Result] =
+ rendering.model.resources.spell_checker.get.flatMap(_.completion(rendering, caret))
+
+ def menu_items(rendering: VSCode_Rendering, caret: Text.Offset): List[Protocol.CompletionItem] =
+ {
+ val model = rendering.model
+ val result =
+ for {
+ spell_checker <- model.resources.spell_checker.get
+ range = rendering.before_caret_range(caret)
+ Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
+ } yield (spell_checker, word)
+
+ result match {
+ case Some((spell_checker, word)) =>
+
+ def item(command: Protocol.Command): Protocol.CompletionItem =
+ Protocol.CompletionItem(
+ label = command.title,
+ text = Some(""),
+ range = Some(model.content.doc.range(Text.Range(caret))),
+ command = Some(command))
+
+ val update_items =
+ if (spell_checker.check(word))
+ List(
+ item(Protocol.Exclude_Word.command),
+ item(Protocol.Exclude_Word_Permanently.command))
+ else
+ List(
+ item(Protocol.Include_Word.command),
+ item(Protocol.Include_Word_Permanently.command))
+
+ val reset_items =
+ spell_checker.reset_enabled() match {
+ case 0 => Nil
+ case n =>
+ val command = Protocol.Reset_Words.command
+ List(item(command).copy(label = command.title + " (" + n + ")"))
+ }
+
+ update_items ::: reset_items
+
+ case None => Nil
+ }
+ }
+}