proper treatment of empty result;

--- a/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jun 20 17:08:24 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jun 20 17:14:27 2017 +0200
@@ -101,16 +101,17 @@
             Completion.Result.merge(history,
               Completion.Result.merge(history, semantic_completion, syntax_completion),
               VSCode_Spell_Checker.completion(rendering, 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.menu_items(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)
         }
     }
   }