1.1 --- a/src/Pure/PIDE/command.scala	Sat Aug 14 22:45:23 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Sat Aug 14 23:01:53 2010 +0200
     1.3 @@ -184,6 +184,6 @@
     1.4  
     1.5    /* accumulated results */
     1.6  
     1.7 -  def empty_state: Command.State =
     1.8 +  val empty_state: Command.State =
     1.9      Command.State(this, Command.Status.UNPROCESSED, 0, Nil, new Markup_Text(Nil, source))
    1.10  }

     2.1 --- a/src/Pure/System/session.scala	Sat Aug 14 22:45:23 2010 +0200
     2.2 +++ b/src/Pure/System/session.scala	Sat Aug 14 23:01:53 2010 +0200
     2.3 @@ -317,7 +317,8 @@
     2.4          def lookup_command(id: Document.Command_ID): Option[Command] =
     2.5            state_snapshot.lookup_command(id)
     2.6          def state(command: Command): Command.State =
     2.7 -          state_snapshot.command_state(document, command)
     2.8 +          try { state_snapshot.command_state(document, command) }
     2.9 +          catch { case _: State.Fail => command.empty_state }
    2.10        }
    2.11      }
    2.12