added spell-checker completion;
authorwenzelm
Mon, 19 Jun 2017 21:33:18 +0200
changeset 66121 070f2be51330
parent 66120 e03ff7e831cc
child 66122 ea7c2a245b84
added spell-checker completion;
src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Mon Jun 19 21:15:06 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Mon Jun 19 21:33:18 2017 +0200
@@ -97,7 +97,11 @@
 
         if (no_completion) Nil
         else {
-          Completion.Result.merge(history, semantic_completion, syntax_completion) match {
+          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 =>
@@ -201,6 +205,9 @@
     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 */