# HG changeset patch # User wenzelm # Date 1262628490 -3600 # Node ID 67733fd0e3fa08078103f692e89008f5361b6fb4 # Parent df9af932e4185e6577c74b6b0305b2097b9df785 back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states; recent_document: require finished state assignment; explicitly typed Session.lookup_command; diff -r df9af932e418 -r 67733fd0e3fa src/Tools/jEdit/src/jedit/document_model.scala --- a/src/Tools/jEdit/src/jedit/document_model.scala Mon Jan 04 00:13:09 2010 +0100 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Mon Jan 04 19:08:10 2010 +0100 @@ -68,7 +68,8 @@ def recent_document(): Document = { def find(change: Change): Document = - if (change.result.is_finished || !change.parent.isDefined) change.document + if (change.result.is_finished && change.document.is_assigned || !change.parent.isDefined) + change.document else find(change.parent.get) find(current_change()) } diff -r df9af932e418 -r 67733fd0e3fa src/Tools/jEdit/src/proofdocument/command.scala --- a/src/Tools/jEdit/src/proofdocument/command.scala Mon Jan 04 00:13:09 2010 +0100 +++ b/src/Tools/jEdit/src/proofdocument/command.scala Mon Jan 04 19:08:10 2010 +0100 @@ -73,7 +73,7 @@ state = state.+(session, message) case Assign => - assigned = true // single assigment + assigned = true // single assignment reply(()) case bad => System.err.println("command accumulator: ignoring bad message " + bad) diff -r df9af932e418 -r 67733fd0e3fa src/Tools/jEdit/src/proofdocument/document.scala --- a/src/Tools/jEdit/src/proofdocument/document.scala Mon Jan 04 00:13:09 2010 +0100 +++ b/src/Tools/jEdit/src/proofdocument/document.scala Mon Jan 04 19:08:10 2010 +0100 @@ -34,7 +34,11 @@ "[()\\[\\]{}:;]", Pattern.MULTILINE) def empty(id: Isar_Document.Document_ID): Document = - new Document(id, Linear_Set(), Map(), Linear_Set(), Map()) + { + val doc = new Document(id, Linear_Set(), Map(), Linear_Set(), Map()) + doc.assign_states(Nil) + doc + } type Structure_Edit = (Option[Command], Option[Command]) type Structure_Change = List[Structure_Edit] @@ -61,46 +65,29 @@ val token_start: Map[Token, Int], // FIXME eliminate val commands: Linear_Set[Command], old_states: Map[Command, Command]) - extends Session.Entity { def content = Token.string_from_tokens(Nil ++ tokens, token_start) - /* accumulated messages */ + /* command/state assignment */ + + val assignment = Future.promise[Map[Command, Command]] + def is_assigned = assignment.is_finished - @volatile private var states = old_states + @volatile private var tmp_states = old_states + + def assign_states(new_states: List[(Command, Command)]) + { + assignment.fulfill(tmp_states ++ new_states) + tmp_states = Map() + } def current_state(cmd: Command): State = - states.getOrElse(cmd, cmd).current_state - - private val accumulator = actor { - loop { - react { - case (session: Session, message: XML.Tree) => - message match { - case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) => - for { - XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) - <- elems - } { - session.lookup_entity(cmd_id) match { - case Some(cmd: Command) => - val state = cmd.assign_state(state_id) - session.register_entity(state) - states += (cmd -> state) - case _ => - } - } - case _ => - } - - case bad => System.err.println("document accumulator: ignoring bad message " + bad) - } - } + { + require(assignment.is_finished) + (assignment.join)(cmd).current_state } - def consume(session: Session, message: XML.Tree) { accumulator ! (session, message) } - /** token view **/ @@ -196,6 +183,8 @@ new_token_start: Map[Token, Int]): Document.Result = { + require(assignment.is_finished) + val new_tokenset = Linear_Set[Token]() ++ new_tokens val cmd_before_change = before_change match { case None => None @@ -273,7 +262,7 @@ val doc = new Document(new_id, new_tokenset, new_token_start, new_commandset, - states -- removed_commands) + assignment.join -- removed_commands) val removes = for (cmd <- removed_commands) yield (cmd_before_change -> None) diff -r df9af932e418 -r 67733fd0e3fa src/Tools/jEdit/src/proofdocument/session.scala --- a/src/Tools/jEdit/src/proofdocument/session.scala Mon Jan 04 00:13:09 2010 +0100 +++ b/src/Tools/jEdit/src/proofdocument/session.scala Mon Jan 04 19:08:10 2010 +0100 @@ -55,8 +55,12 @@ @volatile private var entities = Map[Session.Entity_ID, Session.Entity]() def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id) + def lookup_command(id: Session.Entity_ID): Option[Command] = + lookup_entity(id) match { + case Some(cmd: Command) => Some(cmd) + case _ => None + } - private case class Register(entity: Session.Entity) private case class Start(timeout: Int, args: List[String]) private case object Stop private case class Begin_Document(path: String) @@ -67,6 +71,9 @@ def register(entity: Session.Entity) { entities += (entity.id -> entity) } + var documents = Map[Isar_Document.Document_ID, Document]() + def register_document(doc: Document) { documents += (doc.id -> doc) } + /* document changes */ @@ -80,13 +87,15 @@ (c1.map(_.id).getOrElse(""), c2 match { case None => None - case Some(command) => // FIXME register/define only commands unknown to prover - register(command) - prover.define_command(command.id, system.symbols.encode(command.content)) + case Some(command) => + if (!lookup_command(command.id).isDefined) { + register(command) + prover.define_command(command.id, system.symbols.encode(command.content)) + } Some(command.id) }) } - register(doc) + register_document(doc) prover.edit_document(change.parent.get.id, doc.id, id_changes) } @@ -97,16 +106,35 @@ { raw_results.event(result) + val target_id: Option[Session.Entity_ID] = Position.get_id(result.props) val target: Option[Session.Entity] = - Position.get_id(result.props) match { + target_id match { case None => None - case Some(id) => entities.get(id) + case Some(id) => lookup_entity(id) } if (target.isDefined) target.get.consume(this, result.message) else if (result.kind == Isabelle_Process.Kind.STATUS) { // global status message for (elem <- result.body) { elem match { + // document state assigment + case XML.Elem(Markup.ASSIGN, _, edits) if target_id.isDefined => + documents.get(target_id.get) match { + case Some(doc) => + val states = + for { + XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) + <- edits + cmd <- lookup_command(cmd_id) + } yield { + val st = cmd.assign_state(state_id) + register(st) + (cmd, st) + } + doc.assign_states(states) + case None => + } + // command and keyword declarations case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) => syntax += (name, kind) @@ -167,10 +195,6 @@ loop { react { - case Register(entity: Session.Entity) => - register(entity) - reply(()) - case Start(timeout, args) => if (prover == null) { prover = new Isabelle_Process(system, self, args:_*) with Isar_Document @@ -190,7 +214,7 @@ case Begin_Document(path: String) if prover != null => val id = create_id() val doc = Document.empty(id) - register(doc) + register_document(doc) prover.begin_document(id, path) reply(doc) @@ -209,8 +233,6 @@ /* main methods */ - def register_entity(entity: Session.Entity) { session_actor !? Register(entity) } - def start(timeout: Int, args: List[String]): Option[String] = (session_actor !? Start(timeout, args)).asInstanceOf[Option[String]]