# HG changeset patch # User wenzelm # Date 1281716479 -7200 # Node ID 8b15d0f98962a4239f4cd2c29d0602dfcbd15e0f # Parent 5584ab3d5b13803d8bf17addd2ab14e73864a63b explicit Document.State value, instead of individual state variables in Session, Command, Document; Session.snapshot: pure value based on Document.State; Document.edit_texts: no treatment of state assignment here; diff -r 5584ab3d5b13 -r 8b15d0f98962 src/Pure/Isar/isar_document.scala --- a/src/Pure/Isar/isar_document.scala Fri Aug 13 18:16:50 2010 +0200 +++ b/src/Pure/Isar/isar_document.scala Fri Aug 13 18:21:19 2010 +0200 @@ -12,9 +12,12 @@ /* protocol messages */ object Assign { - def unapply(msg: XML.Tree): Option[List[XML.Tree]] = + def unapply(msg: XML.Tree): Option[List[(Document.Command_ID, Document.Exec_ID)]] = msg match { - case XML.Elem(Markup.Assign, edits) => Some(edits) + case XML.Elem(Markup.Assign, edits) => + val id_edits = edits.map(Edit.unapply) + if (id_edits.forall(_.isDefined)) Some(id_edits.map(_.get)) + else None case _ => None } } diff -r 5584ab3d5b13 -r 8b15d0f98962 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Fri Aug 13 18:16:50 2010 +0200 +++ b/src/Pure/PIDE/command.scala Fri Aug 13 18:21:19 2010 +0200 @@ -40,10 +40,6 @@ val reverse_results: List[XML.Tree], val markup: Markup_Text) { - def this(command: Command) = - this(command, Command.Status.UNPROCESSED, 0, Nil, command.empty_markup) - - /* content */ lazy val results = reverse_results.reverse @@ -154,7 +150,6 @@ val id: Document.Command_ID, val span: Thy_Syntax.Span, val static_parent: Option[Command] = None) // FIXME !? - extends Session.Entity { /* classification */ @@ -178,54 +173,18 @@ lazy val symbol_index = new Symbol.Index(source) - /* accumulated messages */ - - @volatile protected var state = new Command.State(this) - def current_state: Command.State = state - - private case class Consume(message: XML.Tree, forward: Command => Unit) - private case object Assign - - private val accumulator = actor { - var assigned = false - loop { - react { - case Consume(message, forward) if !assigned => - val old_state = state - state = old_state.accumulate(message) - if (!(state eq old_state)) forward(static_parent getOrElse this) - - case Assign => - assigned = true // single assignment - reply(()) - - case bad => System.err.println("Command accumulator: ignoring bad message " + bad) - } - } - } - - def consume(message: XML.Tree, forward: Command => Unit) - { - accumulator ! Consume(message, forward) - } - - def assign_exec(exec_id: Document.Exec_ID): Command = - { - val cmd = new Command(exec_id, span, Some(this)) - accumulator !? Assign - cmd.state = current_state - cmd - } - - /* markup */ - lazy val empty_markup = new Markup_Text(Nil, source) - def markup_node(begin: Int, end: Int, info: Any): Markup_Tree = { val start = symbol_index.decode(begin) val stop = symbol_index.decode(end) new Markup_Tree(new Markup_Node(start, stop, info), Nil) } + + + /* accumulated results */ + + def empty_state: Command.State = + Command.State(this, Command.Status.UNPROCESSED, 0, Nil, new Markup_Text(Nil, source)) } diff -r 5584ab3d5b13 -r 8b15d0f98962 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Fri Aug 13 18:16:50 2010 +0200 +++ b/src/Pure/PIDE/document.scala Fri Aug 13 18:21:19 2010 +0200 @@ -78,12 +78,7 @@ /* initial document */ - val init: Document = - { - val doc = new Document(NO_ID, Map().withDefaultValue(Node.empty), Map()) - doc.assign_execs(Nil) - doc - } + val init: Document = new Document(NO_ID, Map().withDefaultValue(Node.empty)) @@ -102,6 +97,7 @@ val is_outdated: Boolean def convert(offset: Int): Int def revert(offset: Int): Int + def lookup_command(id: Command_ID): Option[Command] def state(command: Command): Command.State } @@ -117,7 +113,6 @@ { val document: Future[Document] = result.map(_._2) def is_finished: Boolean = prev.is_finished && document.is_finished - def is_assigned: Boolean = is_finished && document.join.assignment.is_finished } @@ -127,9 +122,6 @@ def text_edits(session: Session, old_doc: Document, edits: List[Node_Text_Edit]) : (List[Edit[Command]], Document) = { - require(old_doc.assignment.is_finished) - - /* phase 1: edit individual command source */ @tailrec def edit_text(eds: List[Text_Edit], @@ -200,7 +192,6 @@ { val doc_edits = new mutable.ListBuffer[Edit[Command]] var nodes = old_doc.nodes - var former_assignment = old_doc.assignment.join for ((name, text_edits) <- edits) { val commands0 = nodes(name).commands @@ -216,9 +207,107 @@ doc_edits += (name -> Some(cmd_edits)) nodes += (name -> new Node(commands2)) - former_assignment --= removed_commands + } + (doc_edits.toList, new Document(session.create_id(), nodes)) + } + } + + + + /** global state -- accumulated prover results **/ + + class Failed_State(state: State) extends Exception + + object State + { + val init = State().define_document(Document.init, Map()).assign(Document.init.id, Nil) + + class Assignment(former_assignment: Map[Command, Exec_ID]) + { + @volatile private var tmp_assignment = former_assignment + private val promise = Future.promise[Map[Command, Exec_ID]] + def is_finished: Boolean = promise.is_finished + def join: Map[Command, Exec_ID] = promise.join + def assign(command_execs: List[(Command, Exec_ID)]) + { + promise.fulfill(tmp_assignment ++ command_execs) + tmp_assignment = Map() } - (doc_edits.toList, new Document(session.create_id(), nodes, former_assignment)) + } + } + + case class State( + val commands: Map[Command_ID, Command.State] = Map(), + val documents: Map[Version_ID, Document] = Map(), + val execs: Map[Exec_ID, (Command.State, Set[Document])] = Map(), + val assignments: Map[Document, State.Assignment] = Map(), + val disposed: Set[ID] = Set()) // FIXME unused!? + { + private def fail[A]: A = throw new Failed_State(this) + + def define_command(command: Command): State = + { + val id = command.id + if (commands.isDefinedAt(id) || disposed(id)) fail + copy(commands = commands + (id -> command.empty_state)) + } + + def define_document(document: Document, former_assignment: Map[Command, Exec_ID]): State = + { + val id = document.id + if (documents.isDefinedAt(id) || disposed(id)) fail + copy(documents = documents + (id -> document), + assignments = assignments + (document -> new State.Assignment(former_assignment))) + } + + def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command) + def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail) + def the_document(id: Version_ID): Document = documents.getOrElse(id, fail) + def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1 + def the_assignment(document: Document): State.Assignment = assignments.getOrElse(document, fail) + + def accumulate(id: ID, message: XML.Tree): (Command.State, State) = + execs.get(id) match { + case Some((st, docs)) => + val new_st = st.accumulate(message) + (new_st, copy(execs = execs + (id -> (new_st, docs)))) + case None => + commands.get(id) match { + case Some(st) => + val new_st = st.accumulate(message) + (new_st, copy(commands = commands + (id -> new_st))) + case None => fail + } + } + + def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): State = + { + val doc = the_document(id) + val docs = Set(doc) // FIXME unused (!?) + + var new_execs = execs + val assigned_execs = + for ((cmd_id, exec_id) <- edits) yield { + val st = the_command(cmd_id) + if (new_execs.isDefinedAt(exec_id) || disposed(exec_id)) fail + new_execs += (exec_id -> (st, docs)) + (st.command, exec_id) + } + the_assignment(doc).assign(assigned_execs) // FIXME explicit value instead of promise (!?) + copy(execs = new_execs) + } + + def is_assigned(document: Document): Boolean = + assignments.get(document) match { + case Some(assgn) => assgn.is_finished + case None => false + } + + def command_state(document: Document, command: Command): Command.State = + { + val assgn = the_assignment(document) + require(assgn.is_finished) + the_exec_state(assgn.join.getOrElse(command, fail)) } } } @@ -226,28 +315,5 @@ class Document( val id: Document.Version_ID, - val nodes: Map[String, Document.Node], - former_assignment: Map[Command, Command]) // FIXME !? -{ - /* command state assignment */ - - val assignment = Future.promise[Map[Command, Command]] - def await_assignment { assignment.join } - - @volatile private var tmp_assignment = former_assignment + val nodes: Map[String, Document.Node]) - def assign_execs(execs: List[(Command, Command)]) - { - assignment.fulfill(tmp_assignment ++ execs) - tmp_assignment = Map() - } - - def current_state(cmd: Command): Command.State = - { - require(assignment.is_finished) - (assignment.join).get(cmd) match { - case Some(cmd_state) => cmd_state.current_state - case None => new Command.State(cmd, Command.Status.UNDEFINED, 0, Nil, cmd.empty_markup) - } - } -} diff -r 5584ab3d5b13 -r 8b15d0f98962 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Fri Aug 13 18:16:50 2010 +0200 +++ b/src/Pure/System/session.scala Fri Aug 13 18:21:19 2010 +0200 @@ -20,16 +20,6 @@ case object Global_Settings case object Perspective case class Commands_Changed(set: Set[Command]) - - - - /* managed entities */ - - trait Entity - { - val id: Document.ID - def consume(message: XML.Tree, forward: Command => Unit): Unit - } } @@ -72,13 +62,9 @@ @volatile private var syntax = new Outer_Syntax(system.symbols) def current_syntax: Outer_Syntax = syntax - @volatile private var entities = Map[Document.ID, Session.Entity]() - def lookup_entity(id: Document.ID): Option[Session.Entity] = entities.get(id) - def lookup_command(id: Document.ID): Option[Command] = - lookup_entity(id) match { - case Some(cmd: Command) => Some(cmd) - case _ => None - } + @volatile private var global_state = Document.State.init + private def change_state(f: Document.State => Document.State) { global_state = f(global_state) } + def current_state(): Document.State = global_state private case class Started(timeout: Int, args: List[String]) private case object Stop @@ -87,12 +73,6 @@ var prover: Isabelle_Process with Isar_Document = null - def register(entity: Session.Entity) { entities += (entity.id -> entity) } - - var documents = Map[Document.Version_ID, Document]() - def register_document(doc: Document) { documents += (doc.id -> doc) } - register_document(Document.init) - /* document changes */ @@ -101,14 +81,21 @@ { require(change.is_finished) - val old_id = change.prev.join.id + val old_doc = change.prev.join val (node_edits, doc) = change.result.join + var former_assignment = current_state().the_assignment(old_doc).join + for { + (name, Some(cmd_edits)) <- node_edits + (prev, None) <- cmd_edits + removed <- old_doc.nodes(name).commands.get_after(prev) + } former_assignment -= removed + val id_edits = node_edits map { case (name, None) => (name, None) case (name, Some(cmd_edits)) => - val chs = + val ids = cmd_edits map { case (c1, c2) => val id1 = c1.map(_.id) @@ -116,18 +103,18 @@ c2 match { case None => None case Some(command) => - if (!lookup_command(command.id).isDefined) { - register(command) + if (current_state().lookup_command(command.id).isEmpty) { + change_state(_.define_command(command)) prover.define_command(command.id, system.symbols.encode(command.source)) } Some(command.id) } (id1, id2) } - (name -> Some(chs)) + (name -> Some(ids)) } - register_document(doc) - prover.edit_document(old_id, doc.id, id_edits) + change_state(_.define_document(doc, former_assignment)) + prover.edit_document(old_doc.id, doc.id, id_edits) } //}}} @@ -144,47 +131,38 @@ { raw_results.event(result) - val target_id: Option[Document.ID] = Position.get_id(result.properties) - val target: Option[Session.Entity] = - target_id match { - case None => None - case Some(id) => lookup_entity(id) + Position.get_id(result.properties) match { + case Some(target_id) => + try { + val (st, state) = global_state.accumulate(target_id, result.message) + global_state = state + indicate_command_change(st.command) // FIXME forward Command.State (!?) + } + catch { + case _: Document.Failed_State => + if (result.is_status) { + result.body match { + case List(Isar_Document.Assign(edits)) => + try { change_state(_.assign(target_id, edits)) } + catch { case _: Document.Failed_State => bad_result(result) } + case _ => bad_result(result) + } + } + else bad_result(result) + } + case None => + if (result.is_status) { + result.body match { + // keyword declarations // FIXME always global!? + case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind) + case List(Keyword.Keyword_Decl(name)) => syntax += name + case _ => if (!result.is_ready) bad_result(result) + } + } + else if (result.kind == Markup.EXIT) prover = null + else if (result.is_raw) raw_output.event(result) + else if (!result.is_system) bad_result(result) // FIXME syslog for system messages (!?) } - if (target.isDefined) target.get.consume(result.message, indicate_command_change) - else if (result.is_status) { - // global status message - result.body match { - - // execution assignment - case List(Isar_Document.Assign(edits)) if target_id.isDefined => - documents.get(target_id.get) match { - case Some(doc) => - val execs = - for { - Isar_Document.Edit(cmd_id, exec_id) <- edits - cmd <- lookup_command(cmd_id) - } yield { - val st = cmd.assign_exec(exec_id) // FIXME session state - register(st) - (cmd, st) - } - doc.assign_execs(execs) // FIXME session state - case None => bad_result(result) - } - - // keyword declarations - case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind) - case List(Keyword.Keyword_Decl(name)) => syntax += name - - case _ => if (!result.is_ready) bad_result(result) - } - } - else if (result.kind == Markup.EXIT) - prover = null - else if (result.is_raw) - raw_output.event(result) - else if (!result.is_system) // FIXME syslog (!?) - bad_result(result) } //}}} @@ -325,11 +303,14 @@ def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot = { + val state_snapshot = current_state() val history_snapshot = history - require(history_snapshot.exists(_.is_assigned)) + val found_stable = history_snapshot.find(change => + change.is_finished && state_snapshot.is_assigned(change.document.join)) + require(found_stable.isDefined) + val stable = found_stable.get val latest = history_snapshot.head - val stable = history_snapshot.find(_.is_assigned).get val edits = (pending_edits /: history_snapshot.takeWhile(_ != stable))((edits, change) => @@ -342,7 +323,10 @@ val is_outdated = !(pending_edits.isEmpty && latest == stable) def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i)) def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i)) - def state(command: Command): Command.State = document.current_state(command) + def lookup_command(id: Document.Command_ID): Option[Command] = + state_snapshot.lookup_command(id) + def state(command: Command): Command.State = + state_snapshot.command_state(document, command) } } @@ -358,7 +342,7 @@ val result: isabelle.Future[(List[Document.Edit[Command]], Document)] = isabelle.Future.fork { val old_doc = prev.join - old_doc.await_assignment + val former_assignment = current_state().the_assignment(old_doc).join // FIXME async!? Document.text_edits(Session.this, old_doc, edits) } val new_change = new Document.Change(prev, edits, result) diff -r 5584ab3d5b13 -r 8b15d0f98962 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Fri Aug 13 18:16:50 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Fri Aug 13 18:21:19 2010 +0200 @@ -56,8 +56,8 @@ case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) => new External_Hyperlink(begin, end, line, ref_file, ref_line) case Command.RefInfo(_, _, Some(id), Some(offset)) => - Isabelle.session.lookup_entity(id) match { - case Some(ref_cmd: Command) => + snapshot.lookup_command(id) match { // FIXME Command_ID vs. Exec_ID (!??) + case Some(ref_cmd) => snapshot.node.command_start(ref_cmd) match { case Some(ref_cmd_start) => new Internal_Hyperlink(begin, end, line,