1.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Mon Jan 04 00:13:09 2010 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Mon Jan 04 19:08:10 2010 +0100
     1.3 @@ -68,7 +68,8 @@
     1.4    def recent_document(): Document =
     1.5    {
     1.6      def find(change: Change): Document =
     1.7 -      if (change.result.is_finished || !change.parent.isDefined) change.document
     1.8 +      if (change.result.is_finished && change.document.is_assigned || !change.parent.isDefined)
     1.9 +        change.document
    1.10        else find(change.parent.get)
    1.11      find(current_change())
    1.12    }

     2.1 --- a/src/Tools/jEdit/src/proofdocument/command.scala	Mon Jan 04 00:13:09 2010 +0100
     2.2 +++ b/src/Tools/jEdit/src/proofdocument/command.scala	Mon Jan 04 19:08:10 2010 +0100
     2.3 @@ -73,7 +73,7 @@
     2.4            state = state.+(session, message)
     2.5  
     2.6          case Assign =>
     2.7 -          assigned = true  // single assigment
     2.8 +          assigned = true  // single assignment
     2.9            reply(())
    2.10  
    2.11          case bad => System.err.println("command accumulator: ignoring bad message " + bad)

     3.1 --- a/src/Tools/jEdit/src/proofdocument/document.scala	Mon Jan 04 00:13:09 2010 +0100
     3.2 +++ b/src/Tools/jEdit/src/proofdocument/document.scala	Mon Jan 04 19:08:10 2010 +0100
     3.3 @@ -34,7 +34,11 @@
     3.4        "[()\\[\\]{}:;]", Pattern.MULTILINE)
     3.5  
     3.6    def empty(id: Isar_Document.Document_ID): Document =
     3.7 -    new Document(id, Linear_Set(), Map(), Linear_Set(), Map())
     3.8 +  {
     3.9 +    val doc = new Document(id, Linear_Set(), Map(), Linear_Set(), Map())
    3.10 +    doc.assign_states(Nil)
    3.11 +    doc
    3.12 +  }
    3.13  
    3.14    type Structure_Edit = (Option[Command], Option[Command])
    3.15    type Structure_Change = List[Structure_Edit]
    3.16 @@ -61,46 +65,29 @@
    3.17      val token_start: Map[Token, Int],  // FIXME eliminate
    3.18      val commands: Linear_Set[Command],
    3.19      old_states: Map[Command, Command])
    3.20 -  extends Session.Entity
    3.21  {
    3.22    def content = Token.string_from_tokens(Nil ++ tokens, token_start)
    3.23  
    3.24  
    3.25 -  /* accumulated messages */
    3.26 +  /* command/state assignment */
    3.27  
    3.28 -  @volatile private var states = old_states
    3.29 +  val assignment = Future.promise[Map[Command, Command]]
    3.30 +  def is_assigned = assignment.is_finished
    3.31 +
    3.32 +  @volatile private var tmp_states = old_states
    3.33 +
    3.34 +  def assign_states(new_states: List[(Command, Command)])
    3.35 +  {
    3.36 +    assignment.fulfill(tmp_states ++ new_states)
    3.37 +    tmp_states = Map()
    3.38 +  }
    3.39  
    3.40    def current_state(cmd: Command): State =
    3.41 -    states.getOrElse(cmd, cmd).current_state
    3.42 -
    3.43 -  private val accumulator = actor {
    3.44 -    loop {
    3.45 -      react {
    3.46 -        case (session: Session, message: XML.Tree) =>
    3.47 -          message match {
    3.48 -            case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
    3.49 -              for {
    3.50 -                XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
    3.51 -                  <- elems
    3.52 -              } {
    3.53 -                session.lookup_entity(cmd_id) match {
    3.54 -                  case Some(cmd: Command) =>
    3.55 -                    val state = cmd.assign_state(state_id)
    3.56 -                    session.register_entity(state)
    3.57 -                    states += (cmd -> state)
    3.58 -                  case _ =>
    3.59 -                }
    3.60 -              }
    3.61 -            case _ =>
    3.62 -          }
    3.63 -
    3.64 -        case bad => System.err.println("document accumulator: ignoring bad message " + bad)
    3.65 -      }
    3.66 -    }
    3.67 +  {
    3.68 +    require(assignment.is_finished)
    3.69 +    (assignment.join)(cmd).current_state
    3.70    }
    3.71  
    3.72 -  def consume(session: Session, message: XML.Tree) { accumulator ! (session, message) }
    3.73 -
    3.74  
    3.75  
    3.76    /** token view **/
    3.77 @@ -196,6 +183,8 @@
    3.78        new_token_start: Map[Token, Int]):
    3.79      Document.Result =
    3.80    {
    3.81 +    require(assignment.is_finished)
    3.82 +
    3.83      val new_tokenset = Linear_Set[Token]() ++ new_tokens
    3.84      val cmd_before_change = before_change match {
    3.85        case None => None
    3.86 @@ -273,7 +262,7 @@
    3.87  
    3.88      val doc =
    3.89        new Document(new_id, new_tokenset, new_token_start, new_commandset,
    3.90 -        states -- removed_commands)
    3.91 +        assignment.join -- removed_commands)
    3.92  
    3.93      val removes =
    3.94        for (cmd <- removed_commands) yield (cmd_before_change -> None)

     4.1 --- a/src/Tools/jEdit/src/proofdocument/session.scala	Mon Jan 04 00:13:09 2010 +0100
     4.2 +++ b/src/Tools/jEdit/src/proofdocument/session.scala	Mon Jan 04 19:08:10 2010 +0100
     4.3 @@ -55,8 +55,12 @@
     4.4  
     4.5    @volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
     4.6    def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
     4.7 +  def lookup_command(id: Session.Entity_ID): Option[Command] =
     4.8 +    lookup_entity(id) match {
     4.9 +      case Some(cmd: Command) => Some(cmd)
    4.10 +      case _ => None
    4.11 +    }
    4.12  
    4.13 -  private case class Register(entity: Session.Entity)
    4.14    private case class Start(timeout: Int, args: List[String])
    4.15    private case object Stop
    4.16    private case class Begin_Document(path: String)
    4.17 @@ -67,6 +71,9 @@
    4.18  
    4.19      def register(entity: Session.Entity) { entities += (entity.id -> entity) }
    4.20  
    4.21 +    var documents = Map[Isar_Document.Document_ID, Document]()
    4.22 +    def register_document(doc: Document) { documents += (doc.id -> doc) }
    4.23 +
    4.24  
    4.25      /* document changes */
    4.26  
    4.27 @@ -80,13 +87,15 @@
    4.28            (c1.map(_.id).getOrElse(""),
    4.29             c2 match {
    4.30                case None => None
    4.31 -              case Some(command) =>  // FIXME register/define only commands unknown to prover
    4.32 -                register(command)
    4.33 -                prover.define_command(command.id, system.symbols.encode(command.content))
    4.34 +              case Some(command) =>
    4.35 +                if (!lookup_command(command.id).isDefined) {
    4.36 +                  register(command)
    4.37 +                  prover.define_command(command.id, system.symbols.encode(command.content))
    4.38 +                }
    4.39                  Some(command.id)
    4.40              })
    4.41        }
    4.42 -      register(doc)
    4.43 +      register_document(doc)
    4.44        prover.edit_document(change.parent.get.id, doc.id, id_changes)
    4.45      }
    4.46  
    4.47 @@ -97,16 +106,35 @@
    4.48      {
    4.49        raw_results.event(result)
    4.50  
    4.51 +      val target_id: Option[Session.Entity_ID] = Position.get_id(result.props)
    4.52        val target: Option[Session.Entity] =
    4.53 -        Position.get_id(result.props) match {
    4.54 +        target_id match {
    4.55            case None => None
    4.56 -          case Some(id) => entities.get(id)
    4.57 +          case Some(id) => lookup_entity(id)
    4.58          }
    4.59        if (target.isDefined) target.get.consume(this, result.message)
    4.60        else if (result.kind == Isabelle_Process.Kind.STATUS) {
    4.61          // global status message
    4.62          for (elem <- result.body) {
    4.63            elem match {
    4.64 +            // document state assigment
    4.65 +            case XML.Elem(Markup.ASSIGN, _, edits) if target_id.isDefined =>
    4.66 +              documents.get(target_id.get) match {
    4.67 +                case Some(doc) =>
    4.68 +                  val states =
    4.69 +                    for {
    4.70 +                      XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
    4.71 +                        <- edits
    4.72 +                      cmd <- lookup_command(cmd_id)
    4.73 +                    } yield {
    4.74 +                      val st = cmd.assign_state(state_id)
    4.75 +                      register(st)
    4.76 +                      (cmd, st)
    4.77 +                    }
    4.78 +                  doc.assign_states(states)
    4.79 +                case None =>
    4.80 +              }
    4.81 +
    4.82              // command and keyword declarations
    4.83              case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
    4.84                syntax += (name, kind)
    4.85 @@ -167,10 +195,6 @@
    4.86  
    4.87      loop {
    4.88        react {
    4.89 -        case Register(entity: Session.Entity) =>
    4.90 -          register(entity)
    4.91 -          reply(())
    4.92 -
    4.93          case Start(timeout, args) =>
    4.94            if (prover == null) {
    4.95              prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
    4.96 @@ -190,7 +214,7 @@
    4.97          case Begin_Document(path: String) if prover != null =>
    4.98            val id = create_id()
    4.99            val doc = Document.empty(id)
   4.100 -          register(doc)
   4.101 +          register_document(doc)
   4.102            prover.begin_document(id, path)
   4.103            reply(doc)
   4.104  
   4.105 @@ -209,8 +233,6 @@
   4.106  
   4.107    /* main methods */
   4.108  
   4.109 -  def register_entity(entity: Session.Entity) { session_actor !? Register(entity) }
   4.110 -
   4.111    def start(timeout: Int, args: List[String]): Option[String] =
   4.112      (session_actor !? Start(timeout, args)).asInstanceOf[Option[String]]
   4.113