1.1 --- a/src/Pure/PIDE/document.scala	Tue Aug 30 15:49:27 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Tue Aug 30 16:04:26 2011 +0200
     1.3 @@ -191,11 +191,11 @@
     1.4  
     1.5    abstract class Snapshot
     1.6    {
     1.7 +    val state: State
     1.8      val version: Version
     1.9      val node: Node
    1.10      val is_outdated: Boolean
    1.11 -    def find_command(id: Command_ID): Option[(String, Node, Command)]
    1.12 -    def state(command: Command): Command.State
    1.13 +    def command_state(command: Command): Command.State
    1.14      def convert(i: Text.Offset): Text.Offset
    1.15      def convert(range: Text.Range): Text.Range
    1.16      def revert(i: Text.Offset): Text.Offset
    1.17 @@ -269,8 +269,16 @@
    1.18        copy(commands = commands + (id -> command.empty_state))
    1.19      }
    1.20  
    1.21 -    def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command)
    1.22 -    def lookup_exec(id: Exec_ID): Option[Command] = execs.get(id).map(_.command)
    1.23 +    def defined_command(id: Command_ID): Boolean = commands.isDefinedAt(id)
    1.24 +
    1.25 +    def find_command(version: Version, id: ID): Option[(String, Node, Command)] =
    1.26 +      commands.get(id) orElse execs.get(id) match {
    1.27 +        case None => None
    1.28 +        case Some(st) =>
    1.29 +          val command = st.command
    1.30 +          version.nodes.find({ case (_, node) => node.commands(command) })
    1.31 +            .map({ case (name, node) => (name, node, command) })
    1.32 +      }
    1.33  
    1.34      def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
    1.35      def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)  // FIXME rename
    1.36 @@ -367,19 +375,12 @@
    1.37  
    1.38        new Snapshot
    1.39        {
    1.40 +        val state = State.this
    1.41          val version = stable.version.get_finished
    1.42          val node = version.nodes(name)
    1.43          val is_outdated = !(pending_edits.isEmpty && latest == stable)
    1.44  
    1.45 -        def find_command(id: ID): Option[(String, Node, Command)] =
    1.46 -          State.this.lookup_command(id) orElse State.this.lookup_exec(id) match {
    1.47 -            case None => None
    1.48 -            case Some(command) =>
    1.49 -              version.nodes.find({ case (_, node) => node.commands(command) })
    1.50 -                .map({ case (name, node) => (name, node, command) })
    1.51 -          }
    1.52 -
    1.53 -        def state(command: Command): Command.State =
    1.54 +        def command_state(command: Command): Command.State =
    1.55            try {
    1.56              the_exec(the_assignment(version).check_finished.command_execs
    1.57                .getOrElse(command.id, fail))
    1.58 @@ -397,7 +398,7 @@
    1.59            val former_range = revert(range)
    1.60            for {
    1.61              (command, command_start) <- node.command_range(former_range).toStream
    1.62 -            Text.Info(r0, x) <- state(command).markup.
    1.63 +            Text.Info(r0, x) <- command_state(command).markup.
    1.64                select((former_range - command_start).restrict(command.range)) {
    1.65                  case Text.Info(r0, info)
    1.66                  if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) =>