changeset 71601 | 97ccf48c2f0c |
parent 70658 | 4655897b8287 |
child 73344 | f5c147654661 |
--- a/src/Pure/PIDE/document_status.scala Fri Mar 27 13:04:15 2020 +0100 +++ b/src/Pure/PIDE/document_status.scala Fri Mar 27 22:01:27 2020 +0100 @@ -55,7 +55,7 @@ runs = runs) } - val empty = make(Iterator.empty) + val empty: Command_Status = make(Iterator.empty) def merge(status_iterator: Iterator[Command_Status]): Command_Status = if (status_iterator.hasNext) {