# HG changeset patch
# User wenzelm
# Date 1281819713 -7200
# Node ID f3220ef79d51164e8856420b3d44b571d92d8569
# Parent  49f1f657adc26df8e2bba4c3facd93bda23b00bd
Snapshot.state: fall back on Command.empty_state -- looked-up command might be unavailable due to editing divergence;

diff -r 49f1f657adc2 -r f3220ef79d51 src/Pure/PIDE/command.scala
--- 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))
 }
diff -r 49f1f657adc2 -r f3220ef79d51 src/Pure/System/session.scala
--- 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 }
       }
     }