--- 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": {
--- 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())
--- 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<void, void>("PIDE/symbols_request")
+
+
+/* spell checker */
+
+export const include_word_type =
+ new NotificationType<void, void>("PIDE/include_word")
+
+export const include_word_permanently_type =
+ new NotificationType<void, void>("PIDE/include_word_permanently")
+
+export const exclude_word_type =
+ new NotificationType<void, void>("PIDE/exclude_word")
+
+export const exclude_word_permanently_type =
+ new NotificationType<void, void>("PIDE/exclude_word_permanently")
+
+export const reset_words_type =
+ new NotificationType<void, void>("PIDE/reset_words")
--- 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")
--- 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)
--- 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 =>