# HG changeset patch # User wenzelm # Date 1497971304 -7200 # Node ID 81c8bb1d33b97a2da5486d148978699829cea657 # Parent cdb6c10122b6f66d81418e74b12ac8ca50c96445 clarified modules; diff -r cdb6c10122b6 -r 81c8bb1d33b9 src/Pure/build-jars --- 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 ) diff -r cdb6c10122b6 -r 81c8bb1d33b9 src/Tools/VSCode/src/vscode_rendering.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 = { diff -r cdb6c10122b6 -r 81c8bb1d33b9 src/Tools/VSCode/src/vscode_spell_checker.scala --- /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 + } + } +}