# 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) } } }