# HG changeset patch
# User wenzelm
# Date 1497971667 -7200
# Node ID 90629b166203ba8a5a97fecdd72a40a1f7752d4b
# Parent  81c8bb1d33b97a2da5486d148978699829cea657
proper treatment of empty result;

diff -r 81c8bb1d33b9 -r 90629b166203 src/Tools/VSCode/src/vscode_rendering.scala
--- 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)
         }
     }
   }