src/Pure/General/completion.scala
changeset 66151 26eecd42cbc5
parent 66056 cf35abfb9ebc
child 66157 cb57fcdbaf70
--- 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(