# HG changeset patch
# User wenzelm
# Date 1498048220 -7200
# Node ID 26eecd42cbc5aa3ba77c24fcfa691c97b75ec594
# Parent  c2e19b9e13989869273e9eb2fe28bdd8285097ab
tuned signature;

diff -r c2e19b9e1398 -r 26eecd42cbc5 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Wed Jun 21 14:06:16 2017 +0200
+++ b/src/Pure/General/completion.scala	Wed Jun 21 14:30:20 2017 +0200
@@ -42,6 +42,8 @@
             Some(Result(res1.range, res1.original, false, items))
           }
       }
+    def merges(history: History, results: Option[Result]*): Option[Result] =
+      ((None: Option[Result]) /: results)(merge(history, _, _))
   }
 
   sealed case class Result(
diff -r c2e19b9e1398 -r 26eecd42cbc5 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Jun 21 14:06:16 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Jun 21 14:30:20 2017 +0200
@@ -99,8 +99,9 @@
         if (no_completion) Nil
         else {
           val results =
-            Completion.Result.merge(history,
-              Completion.Result.merge(history, semantic_completion, syntax_completion),
+            Completion.Result.merges(history,
+              semantic_completion,
+              syntax_completion,
               VSCode_Spell_Checker.completion(rendering, caret))
           val items =
             results match {
diff -r c2e19b9e1398 -r 26eecd42cbc5 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Wed Jun 21 14:06:16 2017 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Jun 21 14:30:20 2017 +0200
@@ -130,11 +130,10 @@
             rendering.before_caret_range(caret).try_restrict(line_range) match {
               case Some(range) if !range.is_singularity =>
                 val range0 =
-                  Completion.Result.merge(Completion.History.empty,
+                  Completion.Result.merges(Completion.History.empty,
                     syntax_completion(Completion.History.empty, true, Some(rendering)),
-                    Completion.Result.merge(Completion.History.empty,
-                      path_completion(rendering),
-                      JEdit_Bibtex.completion(Completion.History.empty, rendering, caret)))
+                    path_completion(rendering),
+                    JEdit_Bibtex.completion(Completion.History.empty, rendering, caret))
                   .map(_.range)
                 rendering.semantic_completion(range0, range) match {
                   case None => range0
@@ -372,12 +371,11 @@
             opt_rendering match {
               case None => result1
               case Some(rendering) =>
-                Completion.Result.merge(history, result1,
-                  Completion.Result.merge(history,
-                    JEdit_Spell_Checker.completion(rendering, explicit, caret),
-                    Completion.Result.merge(history,
-                      path_completion(rendering),
-                      JEdit_Bibtex.completion(history, rendering, caret))))
+                Completion.Result.merges(history,
+                  result1,
+                  JEdit_Spell_Checker.completion(rendering, explicit, caret),
+                  path_completion(rendering),
+                  JEdit_Bibtex.completion(history, rendering, caret))
             }
           }
           result match {