| changeset 38415 | f3220ef79d51 |
| parent 38373 | e8197eea3cd0 |
| child 38426 | 2858ec7b6dd8 |
--- a/src/Pure/PIDE/command.scala Sat Aug 14 22:45:23 2010 +0200 +++ b/src/Pure/PIDE/command.scala Sat Aug 14 23:01:53 2010 +0200 @@ -184,6 +184,6 @@ /* accumulated results */ - def empty_state: Command.State = + val empty_state: Command.State = Command.State(this, Command.Status.UNPROCESSED, 0, Nil, new Markup_Text(Nil, source)) }