--- 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)
--- 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
)
--- 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": {
--- 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())
--- 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<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 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")
--- 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)
--- 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)(_ :+ _))
--- 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 =>
--- /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
+ }
+ }
+}
--- 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 =