# HG changeset patch # User wenzelm # Date 1497963874 -7200 # Node ID f7ef4c50b7471ab49c99cda1991128ab9ff0710f # Parent d2923067b3760083b22fa74c0183ba2a0a3337dc added commands for spell-checker dictionary; diff -r d2923067b376 -r f7ef4c50b747 src/Tools/VSCode/extension/package.json --- a/src/Tools/VSCode/extension/package.json Tue Jun 20 11:19:06 2017 +0200 +++ b/src/Tools/VSCode/extension/package.json Tue Jun 20 15:04:34 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 d2923067b376 -r f7ef4c50b747 src/Tools/VSCode/extension/src/extension.ts --- a/src/Tools/VSCode/extension/src/extension.ts Tue Jun 20 11:19:06 2017 +0200 +++ b/src/Tools/VSCode/extension/src/extension.ts Tue Jun 20 15:04:34 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 d2923067b376 -r f7ef4c50b747 src/Tools/VSCode/extension/src/protocol.ts --- a/src/Tools/VSCode/extension/src/protocol.ts Tue Jun 20 11:19:06 2017 +0200 +++ b/src/Tools/VSCode/extension/src/protocol.ts Tue Jun 20 15:04:34 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 d2923067b376 -r f7ef4c50b747 src/Tools/VSCode/src/protocol.scala --- a/src/Tools/VSCode/src/protocol.scala Tue Jun 20 11:19:06 2017 +0200 +++ b/src/Tools/VSCode/src/protocol.scala Tue Jun 20 15:04:34 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 @@ -323,7 +332,8 @@ detail: Option[String] = None, documentation: Option[String] = None, insertText: Option[String] = None, - range: Option[Line.Range] = None) + range: Option[Line.Range] = None, + command: Option[Command] = None) { def json: JSON.T = Map("label" -> label) ++ @@ -333,7 +343,8 @@ JSON.optional("insertText" -> insertText) ++ 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" -> insertText.getOrElse(label)))) ++ + JSON.optional("command" -> command.map(_.json)) } object Completion extends RequestTextDocumentPosition("textDocument/completion") @@ -343,6 +354,15 @@ } + /* spell checker */ + + object Include_Word extends Notification0("PIDE/include_word") + object Include_Word_Permanently extends Notification0("PIDE/include_word_permanently") + object Exclude_Word extends Notification0("PIDE/exclude_word") + object Exclude_Word_Permanently extends Notification0("PIDE/exclude_word_permanently") + object Reset_Words extends Notification0("PIDE/reset_words") + + /* hover request */ object Hover extends RequestTextDocumentPosition("textDocument/hover") diff -r d2923067b376 -r f7ef4c50b747 src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Tue Jun 20 11:19:06 2017 +0200 +++ b/src/Tools/VSCode/src/server.scala Tue Jun 20 15:04:34 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 d2923067b376 -r f7ef4c50b747 src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Tue Jun 20 11:19:06 2017 +0200 +++ b/src/Tools/VSCode/src/vscode_resources.scala Tue Jun 20 15:04:34 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 =>