# HG changeset patch # User wenzelm # Date 1497972689 -7200 # Node ID 8f1cbb77a70a1b14d4b1f306abbaf8c0a89b0a16 # Parent dd006934a7195d982ce4c0573bd419665b8f4e17# Parent 51f74025a3e366da2e7d0352ff710e6ce06485ae merged diff -r dd006934a719 -r 8f1cbb77a70a src/Pure/Tools/spell_checker.scala --- a/src/Pure/Tools/spell_checker.scala Tue Jun 20 14:41:35 2017 +0200 +++ b/src/Pure/Tools/spell_checker.scala Tue Jun 20 17:31:29 2017 +0200 @@ -248,8 +248,6 @@ result.getOrElse(Nil).map(recover_case) } - def complete_enabled(word: String): Boolean = complete(word).nonEmpty - def completion(rendering: Rendering, caret: Text.Offset): Option[Completion.Result] = { val caret_range = rendering.before_caret_range(caret) @@ -264,7 +262,6 @@ } } - class Spell_Checker_Variable { private val no_spell_checker: (String, Option[Spell_Checker]) = ("", None) diff -r dd006934a719 -r 8f1cbb77a70a src/Pure/build-jars --- a/src/Pure/build-jars Tue Jun 20 14:41:35 2017 +0200 +++ b/src/Pure/build-jars Tue Jun 20 17:31:29 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 dd006934a719 -r 8f1cbb77a70a src/Tools/VSCode/extension/package.json --- a/src/Tools/VSCode/extension/package.json Tue Jun 20 14:41:35 2017 +0200 +++ b/src/Tools/VSCode/extension/package.json Tue Jun 20 17:31:29 2017 +0200 @@ -72,6 +72,31 @@ "light": "./media/ViewSource.svg", "dark": "./media/ViewSource_inverse.svg" } + }, + { + "command": "isabelle.include-word", + "title": "Include word", + "category": "Isabelle" + }, + { + "command": "isabelle.include-word-permanently", + "title": "Include word permanently", + "category": "Isabelle" + }, + { + "command": "isabelle.exclude-word", + "title": "Exclude word", + "category": "Isabelle" + }, + { + "command": "isabelle.exclude-word-permanently", + "title": "Exclude word permanently", + "category": "Isabelle" + }, + { + "command": "isabelle.reset-words", + "title": "Reset non-permanent words", + "category": "Isabelle" } ], "menus": { diff -r dd006934a719 -r 8f1cbb77a70a src/Tools/VSCode/extension/src/extension.ts --- a/src/Tools/VSCode/extension/src/extension.ts Tue Jun 20 14:41:35 2017 +0200 +++ b/src/Tools/VSCode/extension/src/extension.ts Tue Jun 20 17:31:29 2017 +0200 @@ -141,6 +141,25 @@ languages.registerCompletionItemProvider(mode, completion_provider)) } + + /* spell checker */ + + language_client.onReady().then(() => + { + context.subscriptions.push( + commands.registerCommand("isabelle.include-word", uri => + language_client.sendNotification(protocol.include_word_type)), + commands.registerCommand("isabelle.include-word-permanently", uri => + language_client.sendNotification(protocol.include_word_permanently_type)), + commands.registerCommand("isabelle.exclude-word", uri => + language_client.sendNotification(protocol.exclude_word_type)), + commands.registerCommand("isabelle.exclude-word-permanently", uri => + language_client.sendNotification(protocol.exclude_word_permanently_type)), + commands.registerCommand("isabelle.reset-words", uri => + language_client.sendNotification(protocol.reset_words_type))) + }) + + /* start server */ context.subscriptions.push(language_client.start()) diff -r dd006934a719 -r 8f1cbb77a70a src/Tools/VSCode/extension/src/protocol.ts --- a/src/Tools/VSCode/extension/src/protocol.ts Tue Jun 20 14:41:35 2017 +0200 +++ b/src/Tools/VSCode/extension/src/protocol.ts Tue Jun 20 17:31:29 2017 +0200 @@ -104,3 +104,21 @@ export const symbols_request_type = new NotificationType("PIDE/symbols_request") + + +/* spell checker */ + +export const include_word_type = + new NotificationType("PIDE/include_word") + +export const include_word_permanently_type = + new NotificationType("PIDE/include_word_permanently") + +export const exclude_word_type = + new NotificationType("PIDE/exclude_word") + +export const exclude_word_permanently_type = + new NotificationType("PIDE/exclude_word_permanently") + +export const reset_words_type = + new NotificationType("PIDE/reset_words") diff -r dd006934a719 -r 8f1cbb77a70a src/Tools/VSCode/src/protocol.scala --- a/src/Tools/VSCode/src/protocol.scala Tue Jun 20 14:41:35 2017 +0200 +++ b/src/Tools/VSCode/src/protocol.scala Tue Jun 20 17:31:29 2017 +0200 @@ -258,6 +258,15 @@ } + /* commands */ + + sealed case class Command(title: String, command: String, arguments: List[JSON.T] = Nil) + { + def json: JSON.T = + Map("title" -> title, "command" -> command, "arguments" -> arguments) + } + + /* document edits */ object DidOpenTextDocument @@ -322,18 +331,20 @@ kind: Option[Int] = None, detail: Option[String] = None, documentation: Option[String] = None, - insertText: Option[String] = None, - range: Option[Line.Range] = None) + text: Option[String] = None, + range: Option[Line.Range] = None, + command: Option[Command] = None) { def json: JSON.T = Map("label" -> label) ++ JSON.optional("kind" -> kind) ++ JSON.optional("detail" -> detail) ++ JSON.optional("documentation" -> documentation) ++ - JSON.optional("insertText" -> insertText) ++ + JSON.optional("insertText" -> text) ++ JSON.optional("range" -> range.map(Range(_))) ++ JSON.optional("textEdit" -> - range.map(r => Map("range" -> Range(r), "newText" -> insertText.getOrElse(label)))) + range.map(r => Map("range" -> Range(r), "newText" -> text.getOrElse(label)))) ++ + JSON.optional("command" -> command.map(_.json)) } object Completion extends RequestTextDocumentPosition("textDocument/completion") @@ -343,6 +354,34 @@ } + /* spell checker */ + + object Include_Word extends Notification0("PIDE/include_word") + { + val command = Command("Include word", "isabelle.include-word") + } + + object Include_Word_Permanently extends Notification0("PIDE/include_word_permanently") + { + val command = Command("Include word permanently", "isabelle.include-word-permanently") + } + + object Exclude_Word extends Notification0("PIDE/exclude_word") + { + val command = Command("Exclude word", "isabelle.exclude-word") + } + + object Exclude_Word_Permanently extends Notification0("PIDE/exclude_word_permanently") + { + val command = Command("Exclude word permanently", "isabelle.exclude-word-permanently") + } + + object Reset_Words extends Notification0("PIDE/reset_words") + { + val command = Command("Reset non-permanent words", "isabelle.reset-words") + } + + /* hover request */ object Hover extends RequestTextDocumentPosition("textDocument/hover") diff -r dd006934a719 -r 8f1cbb77a70a src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Tue Jun 20 14:41:35 2017 +0200 +++ b/src/Tools/VSCode/src/server.scala Tue Jun 20 17:31:29 2017 +0200 @@ -208,11 +208,22 @@ if (resources.flush_output(channel)) delay_output.invoke() } + def update_output(changed_nodes: Traversable[JFile]) + { + resources.update_output(changed_nodes) + delay_output.invoke() + } + + def update_output_visible() + { + resources.update_output_visible() + delay_output.invoke() + } + private val prover_output = Session.Consumer[Session.Commands_Changed](getClass.getName) { case changed => - resources.update_output(changed.nodes.toList.map(resources.node_file(_))) - delay_output.invoke() + update_output(changed.nodes.toList.map(resources.node_file(_))) } private val syslog = @@ -337,6 +348,32 @@ } + /* spell-checker dictionary */ + + def update_dictionary(include: Boolean, permanent: Boolean) + { + for { + spell_checker <- resources.spell_checker.get + caret <- resources.get_caret() + rendering = caret.model.rendering() + range = rendering.before_caret_range(caret.offset) + Text.Info(_, word) <- Spell_Checker.current_word(rendering, range) + } { + spell_checker.update(word, include, permanent) + update_output_visible() + } + } + + def reset_dictionary() + { + for (spell_checker <- resources.spell_checker.get) + { + spell_checker.reset() + update_output_visible() + } + } + + /* hover */ def hover(id: Protocol.Id, node_pos: Line.Node_Position) @@ -400,6 +437,11 @@ case Protocol.DidChangeTextDocument(file, _, changes) => change_document(file, changes) case Protocol.DidCloseTextDocument(file) => close_document(file) case Protocol.Completion(id, node_pos) => completion(id, node_pos) + case Protocol.Include_Word(()) => update_dictionary(true, false) + case Protocol.Include_Word_Permanently(()) => update_dictionary(true, true) + case Protocol.Exclude_Word(()) => update_dictionary(false, false) + case Protocol.Exclude_Word_Permanently(()) => update_dictionary(false, true) + case Protocol.Reset_Words(()) => reset_dictionary() case Protocol.Hover(id, node_pos) => hover(id, node_pos) case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos) case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos) diff -r dd006934a719 -r 8f1cbb77a70a src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala Tue Jun 20 14:41:35 2017 +0200 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Tue Jun 20 17:31:29 2017 +0200 @@ -71,6 +71,7 @@ rendering => def model: Document_Model = _model + def resources: VSCode_Resources = model.resources /* completion */ @@ -100,16 +101,18 @@ val results = Completion.Result.merge(history, Completion.Result.merge(history, semantic_completion, syntax_completion), - spell_checker_completion(caret)) - results match { - case None => Nil - case Some(result) => - result.items.map(item => - Protocol.CompletionItem( - label = item.replacement, - detail = Some(item.description.mkString(" ")), - range = Some(doc.range(item.range)))) - } + VSCode_Spell_Checker.completion(rendering, caret)) + val items = + results match { + case None => Nil + case Some(result) => + result.items.map(item => + Protocol.CompletionItem( + label = item.replacement, + detail = Some(item.description.mkString(" ")), + range = Some(doc.range(item.range)))) + } + items ::: VSCode_Spell_Checker.menu_items(rendering, caret) } } } @@ -134,7 +137,7 @@ range = model.content.doc.range(text_range) (_, XML.Elem(Markup(name, _), body)) <- res.iterator } yield { - val message = model.resources.output_pretty_message(body) + val message = resources.output_pretty_message(body) val severity = VSCode_Rendering.message_severity.get(name) Protocol.Diagnostic(range, message, severity = severity) }).toList @@ -191,24 +194,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)) - - /* decorations */ def decorations: List[Document_Model.Decoration] = // list of canonical length and order @@ -229,7 +214,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 = { @@ -238,7 +223,7 @@ yield { val range = model.content.doc.range(text_range) Protocol.DecorationOpts(range, - msgs.map(msg => Protocol.MarkedString(model.resources.output_pretty_tooltip(msg)))) + msgs.map(msg => Protocol.MarkedString(resources.output_pretty_tooltip(msg)))) } Protocol.Decoration(decoration.typ, content) } @@ -255,7 +240,7 @@ : Option[Line.Node_Range] = { for { - platform_path <- model.resources.source_file(source_name) + platform_path <- resources.source_file(source_name) file <- (try { Some(new JFile(platform_path).getCanonicalFile) } catch { case ERROR(_) => None }) @@ -263,7 +248,7 @@ yield { Line.Node_Range(file.getPath, if (range.start > 0) { - model.resources.get_file_content(file) match { + resources.get_file_content(file) match { case Some(text) => val chunk = Symbol.Text_Chunk(text) val doc = Line.Document(text) @@ -318,7 +303,7 @@ case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) => val iterator = for { - Text.Info(entry_range, (entry, model)) <- model.resources.bibtex_entries_iterator + Text.Info(entry_range, (entry, model)) <- resources.bibtex_entries_iterator if entry == name } yield Line.Node_Range(model.node_name.node, model.content.doc.range(entry_range)) if (iterator.isEmpty) None else Some((links /: iterator)(_ :+ _)) diff -r dd006934a719 -r 8f1cbb77a70a src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Tue Jun 20 14:41:35 2017 +0200 +++ b/src/Tools/VSCode/src/vscode_resources.scala Tue Jun 20 17:31:29 2017 +0200 @@ -285,6 +285,10 @@ def update_output(changed_nodes: Traversable[JFile]): Unit = state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes)) + def update_output_visible(): Unit = + state.change(st => st.copy(pending_output = st.pending_output ++ + (for ((file, model) <- st.models.iterator if model.node_visible) yield file))) + def flush_output(channel: Channel): Boolean = { state.change_result(st => diff -r dd006934a719 -r 8f1cbb77a70a 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:31:29 2017 +0200 @@ -0,0 +1,73 @@ +/* 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 <- rendering.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.resources.spell_checker.get.flatMap(_.completion(rendering, caret)) + + def menu_items(rendering: VSCode_Rendering, caret: Text.Offset): List[Protocol.CompletionItem] = + { + val result = + for { + spell_checker <- rendering.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(rendering.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 + } + } +} diff -r dd006934a719 -r 8f1cbb77a70a src/Tools/jEdit/src/jedit_spell_checker.scala --- a/src/Tools/jEdit/src/jedit_spell_checker.scala Tue Jun 20 14:41:35 2017 +0200 +++ b/src/Tools/jEdit/src/jedit_spell_checker.scala Tue Jun 20 17:31:29 2017 +0200 @@ -53,7 +53,7 @@ new EnhancedMenuItem(context.getAction(name).getLabel, name, context) val complete_items = - if (spell_checker.complete_enabled(word)) List(item("isabelle.complete-word")) + if (spell_checker.complete(word).nonEmpty) List(item("isabelle.complete-word")) else Nil val update_items =