--- 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(
--- 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),
--- 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),