# HG changeset patch
# User wenzelm
# Date 1498072251 -7200
# Node ID cb57fcdbaf7013ddc582914552b0eb8e4ff158b0
# Parent  2463cba9f18f0b82a6daa9adf5adc0550a339238
tuned signature;

diff -r 2463cba9f18f -r cb57fcdbaf70 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Tue Jun 20 21:41:59 2017 +0200
+++ b/src/Pure/General/completion.scala	Wed Jun 21 21:10:51 2017 +0200
@@ -31,19 +31,17 @@
   object Result
   {
     def empty(range: Text.Range): Result = Result(range, "", false, Nil)
-    def merge(history: History, result1: Option[Result], result2: Option[Result]): Option[Result] =
-      (result1, result2) match {
-        case (_, None) => result1
-        case (None, _) => result2
-        case (Some(res1), Some(res2)) =>
+    def merge(history: History, results: Option[Result]*): Option[Result] =
+      ((None: Option[Result]) /: results)({
+        case (result1, None) => result1
+        case (None, result2) => result2
+        case (result1 @ Some(res1), Some(res2)) =>
           if (res1.range != res2.range || res1.original != res2.original) result1
           else {
             val items = (res1.items ::: res2.items).sorted(history.ordering)
             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 2463cba9f18f -r cb57fcdbaf70 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jun 20 21:41:59 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Jun 21 21:10:51 2017 +0200
@@ -108,7 +108,7 @@
         if (no_completion) Nil
         else {
           val results =
-            Completion.Result.merges(history,
+            Completion.Result.merge(history,
               semantic_completion,
               syntax_completion,
               VSCode_Spell_Checker.completion(rendering, caret),
diff -r 2463cba9f18f -r cb57fcdbaf70 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Tue Jun 20 21:41:59 2017 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Jun 21 21:10:51 2017 +0200
@@ -130,7 +130,7 @@
             rendering.before_caret_range(caret).try_restrict(line_range) match {
               case Some(range) if !range.is_singularity =>
                 val range0 =
-                  Completion.Result.merges(Completion.History.empty,
+                  Completion.Result.merge(Completion.History.empty,
                     syntax_completion(Completion.History.empty, true, Some(rendering)),
                     path_completion(rendering),
                     Document_Model.bibtex_completion(Completion.History.empty, rendering, caret))
@@ -371,7 +371,7 @@
             opt_rendering match {
               case None => result1
               case Some(rendering) =>
-                Completion.Result.merges(history,
+                Completion.Result.merge(history,
                   result1,
                   JEdit_Spell_Checker.completion(rendering, explicit, caret),
                   path_completion(rendering),