src/Pure/PIDE/document.scala
changeset 47395 e6261a493f04
parent 47388 fe4b245af74c
child 48706 e2b512024eab
     1.1 --- a/src/Pure/PIDE/document.scala	Sat Apr 07 18:08:29 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Apr 07 19:28:44 2012 +0200
     1.3 @@ -364,7 +364,7 @@
     1.4        }
     1.5  
     1.6      def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
     1.7 -    def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)  // FIXME rename
     1.8 +    def the_command_state(id: Command_ID): Command.State = commands.getOrElse(id, fail)
     1.9      def the_exec(id: Exec_ID): Command.State = execs.getOrElse(id, fail)
    1.10      def the_assignment(version: Version): State.Assignment =
    1.11        assignments.getOrElse(version.id, fail)
    1.12 @@ -390,7 +390,7 @@
    1.13        val (changed_commands, new_execs) =
    1.14          ((Nil: List[Command], execs) /: command_execs) {
    1.15            case ((commands1, execs1), (cmd_id, exec)) =>
    1.16 -            val st = the_command(cmd_id)
    1.17 +            val st = the_command_state(cmd_id)
    1.18              val commands2 = st.command :: commands1
    1.19              val execs2 =
    1.20                exec match {
    1.21 @@ -470,7 +470,11 @@
    1.22          the_exec(the_assignment(version).check_finished.command_execs
    1.23            .getOrElse(command.id, fail))
    1.24        }
    1.25 -      catch { case _: State.Fail => command.empty_state }
    1.26 +      catch {
    1.27 +        case _: State.Fail =>
    1.28 +          try { the_command_state(command.id) }
    1.29 +          catch { case _: State.Fail => command.empty_state }
    1.30 +      }
    1.31      }
    1.32  
    1.33