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(