provide spell-checker menu via completion commands;

--- a/src/Tools/VSCode/src/protocol.scala	Tue Jun 20 15:04:34 2017 +0200
+++ b/src/Tools/VSCode/src/protocol.scala	Tue Jun 20 16:14:38 2017 +0200
@@ -357,10 +357,29 @@
   /* 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 */

--- a/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jun 20 15:04:34 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jun 20 16:14:38 2017 +0200
@@ -108,7 +108,8 @@
                 Protocol.CompletionItem(
                   label = item.replacement,
                   detail = Some(item.description.mkString(" ")),
-                  range = Some(doc.range(item.range))))
+                  range = Some(doc.range(item.range)))) :::
+              spell_checker_menu(caret)
           }
         }
     }
@@ -208,6 +209,49 @@
   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,
+            insertText = 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 */