changeset 38415 | f3220ef79d51 |
parent 38414 | 49f1f657adc2 |
child 38416 | 56e76cd46b4f |
--- a/src/Pure/System/session.scala Sat Aug 14 22:45:23 2010 +0200 +++ b/src/Pure/System/session.scala Sat Aug 14 23:01:53 2010 +0200 @@ -317,7 +317,8 @@ def lookup_command(id: Document.Command_ID): Option[Command] = state_snapshot.lookup_command(id) def state(command: Command): Command.State = - state_snapshot.command_state(document, command) + try { state_snapshot.command_state(document, command) } + catch { case _: State.Fail => command.empty_state } } }