1.1 --- a/src/Pure/PIDE/document.scala	Thu Aug 12 14:22:23 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Aug 12 15:19:11 2010 +0200
     1.3 @@ -16,14 +16,15 @@
     1.4  {
     1.5    /* formal identifiers */
     1.6  
     1.7 -  type Version_ID = Long
     1.8 -  type Command_ID = Long
     1.9 -  type State_ID = Long
    1.10 +  type ID = Long
    1.11 +  type Exec_ID = ID
    1.12 +  type Command_ID = ID
    1.13 +  type Version_ID = ID
    1.14  
    1.15 -  val NO_ID = 0L
    1.16 +  val NO_ID: ID = 0
    1.17  
    1.18 -  def parse_id(s: String): Long = java.lang.Long.parseLong(s)
    1.19 -  def print_id(id: Long): String = id.toString
    1.20 +  def parse_id(s: String): ID = java.lang.Long.parseLong(s)
    1.21 +  def print_id(id: ID): String = id.toString
    1.22  
    1.23  
    1.24  
    1.25 @@ -80,7 +81,7 @@
    1.26    val init: Document =
    1.27    {
    1.28      val doc = new Document(NO_ID, Map().withDefaultValue(Node.empty), Map())
    1.29 -    doc.assign_states(Nil)
    1.30 +    doc.assign_execs(Nil)
    1.31      doc
    1.32    }
    1.33  
    1.34 @@ -239,7 +240,7 @@
    1.35      {
    1.36        val doc_edits = new mutable.ListBuffer[Edit[Command]]
    1.37        var nodes = old_doc.nodes
    1.38 -      var former_states = old_doc.assignment.join
    1.39 +      var former_assignment = old_doc.assignment.join
    1.40  
    1.41        for ((name, text_edits) <- edits) {
    1.42          val commands0 = nodes(name).commands
    1.43 @@ -255,9 +256,9 @@
    1.44  
    1.45          doc_edits += (name -> Some(cmd_edits))
    1.46          nodes += (name -> new Node(commands2))
    1.47 -        former_states --= removed_commands
    1.48 +        former_assignment --= removed_commands
    1.49        }
    1.50 -      (doc_edits.toList, new Document(new_id, nodes, former_states))
    1.51 +      (doc_edits.toList, new Document(new_id, nodes, former_assignment))
    1.52      }
    1.53    }
    1.54  }
    1.55 @@ -266,19 +267,19 @@
    1.56  class Document(
    1.57      val id: Document.Version_ID,
    1.58      val nodes: Map[String, Document.Node],
    1.59 -    former_states: Map[Command, Command])  // FIXME !?
    1.60 +    former_assignment: Map[Command, Command])  // FIXME !?
    1.61  {
    1.62    /* command state assignment */
    1.63  
    1.64    val assignment = Future.promise[Map[Command, Command]]
    1.65    def await_assignment { assignment.join }
    1.66  
    1.67 -  @volatile private var tmp_states = former_states
    1.68 +  @volatile private var tmp_assignment = former_assignment
    1.69  
    1.70 -  def assign_states(new_states: List[(Command, Command)])
    1.71 +  def assign_execs(execs: List[(Command, Command)])
    1.72    {
    1.73 -    assignment.fulfill(tmp_states ++ new_states)
    1.74 -    tmp_states = Map()
    1.75 +    assignment.fulfill(tmp_assignment ++ execs)
    1.76 +    tmp_assignment = Map()
    1.77    }
    1.78  
    1.79    def current_state(cmd: Command): Command.State =