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;
--- 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
}
}
--- 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))
}
--- 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)
- }
- }
-}
--- 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)
--- 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,