1.1 --- a/src/Pure/PIDE/document.scala Fri Aug 13 18:16:50 2010 +0200
1.2 +++ b/src/Pure/PIDE/document.scala Fri Aug 13 18:21:19 2010 +0200
1.3 @@ -78,12 +78,7 @@
1.4
1.5 /* initial document */
1.6
1.7 - val init: Document =
1.8 - {
1.9 - val doc = new Document(NO_ID, Map().withDefaultValue(Node.empty), Map())
1.10 - doc.assign_execs(Nil)
1.11 - doc
1.12 - }
1.13 + val init: Document = new Document(NO_ID, Map().withDefaultValue(Node.empty))
1.14
1.15
1.16
1.17 @@ -102,6 +97,7 @@
1.18 val is_outdated: Boolean
1.19 def convert(offset: Int): Int
1.20 def revert(offset: Int): Int
1.21 + def lookup_command(id: Command_ID): Option[Command]
1.22 def state(command: Command): Command.State
1.23 }
1.24
1.25 @@ -117,7 +113,6 @@
1.26 {
1.27 val document: Future[Document] = result.map(_._2)
1.28 def is_finished: Boolean = prev.is_finished && document.is_finished
1.29 - def is_assigned: Boolean = is_finished && document.join.assignment.is_finished
1.30 }
1.31
1.32
1.33 @@ -127,9 +122,6 @@
1.34 def text_edits(session: Session, old_doc: Document, edits: List[Node_Text_Edit])
1.35 : (List[Edit[Command]], Document) =
1.36 {
1.37 - require(old_doc.assignment.is_finished)
1.38 -
1.39 -
1.40 /* phase 1: edit individual command source */
1.41
1.42 @tailrec def edit_text(eds: List[Text_Edit],
1.43 @@ -200,7 +192,6 @@
1.44 {
1.45 val doc_edits = new mutable.ListBuffer[Edit[Command]]
1.46 var nodes = old_doc.nodes
1.47 - var former_assignment = old_doc.assignment.join
1.48
1.49 for ((name, text_edits) <- edits) {
1.50 val commands0 = nodes(name).commands
1.51 @@ -216,9 +207,107 @@
1.52
1.53 doc_edits += (name -> Some(cmd_edits))
1.54 nodes += (name -> new Node(commands2))
1.55 - former_assignment --= removed_commands
1.56 }
1.57 - (doc_edits.toList, new Document(session.create_id(), nodes, former_assignment))
1.58 + (doc_edits.toList, new Document(session.create_id(), nodes))
1.59 + }
1.60 + }
1.61 +
1.62 +
1.63 +
1.64 + /** global state -- accumulated prover results **/
1.65 +
1.66 + class Failed_State(state: State) extends Exception
1.67 +
1.68 + object State
1.69 + {
1.70 + val init = State().define_document(Document.init, Map()).assign(Document.init.id, Nil)
1.71 +
1.72 + class Assignment(former_assignment: Map[Command, Exec_ID])
1.73 + {
1.74 + @volatile private var tmp_assignment = former_assignment
1.75 + private val promise = Future.promise[Map[Command, Exec_ID]]
1.76 + def is_finished: Boolean = promise.is_finished
1.77 + def join: Map[Command, Exec_ID] = promise.join
1.78 + def assign(command_execs: List[(Command, Exec_ID)])
1.79 + {
1.80 + promise.fulfill(tmp_assignment ++ command_execs)
1.81 + tmp_assignment = Map()
1.82 + }
1.83 + }
1.84 + }
1.85 +
1.86 + case class State(
1.87 + val commands: Map[Command_ID, Command.State] = Map(),
1.88 + val documents: Map[Version_ID, Document] = Map(),
1.89 + val execs: Map[Exec_ID, (Command.State, Set[Document])] = Map(),
1.90 + val assignments: Map[Document, State.Assignment] = Map(),
1.91 + val disposed: Set[ID] = Set()) // FIXME unused!?
1.92 + {
1.93 + private def fail[A]: A = throw new Failed_State(this)
1.94 +
1.95 + def define_command(command: Command): State =
1.96 + {
1.97 + val id = command.id
1.98 + if (commands.isDefinedAt(id) || disposed(id)) fail
1.99 + copy(commands = commands + (id -> command.empty_state))
1.100 + }
1.101 +
1.102 + def define_document(document: Document, former_assignment: Map[Command, Exec_ID]): State =
1.103 + {
1.104 + val id = document.id
1.105 + if (documents.isDefinedAt(id) || disposed(id)) fail
1.106 + copy(documents = documents + (id -> document),
1.107 + assignments = assignments + (document -> new State.Assignment(former_assignment)))
1.108 + }
1.109 +
1.110 + def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command)
1.111 + def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
1.112 + def the_document(id: Version_ID): Document = documents.getOrElse(id, fail)
1.113 + def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
1.114 + def the_assignment(document: Document): State.Assignment = assignments.getOrElse(document, fail)
1.115 +
1.116 + def accumulate(id: ID, message: XML.Tree): (Command.State, State) =
1.117 + execs.get(id) match {
1.118 + case Some((st, docs)) =>
1.119 + val new_st = st.accumulate(message)
1.120 + (new_st, copy(execs = execs + (id -> (new_st, docs))))
1.121 + case None =>
1.122 + commands.get(id) match {
1.123 + case Some(st) =>
1.124 + val new_st = st.accumulate(message)
1.125 + (new_st, copy(commands = commands + (id -> new_st)))
1.126 + case None => fail
1.127 + }
1.128 + }
1.129 +
1.130 + def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): State =
1.131 + {
1.132 + val doc = the_document(id)
1.133 + val docs = Set(doc) // FIXME unused (!?)
1.134 +
1.135 + var new_execs = execs
1.136 + val assigned_execs =
1.137 + for ((cmd_id, exec_id) <- edits) yield {
1.138 + val st = the_command(cmd_id)
1.139 + if (new_execs.isDefinedAt(exec_id) || disposed(exec_id)) fail
1.140 + new_execs += (exec_id -> (st, docs))
1.141 + (st.command, exec_id)
1.142 + }
1.143 + the_assignment(doc).assign(assigned_execs) // FIXME explicit value instead of promise (!?)
1.144 + copy(execs = new_execs)
1.145 + }
1.146 +
1.147 + def is_assigned(document: Document): Boolean =
1.148 + assignments.get(document) match {
1.149 + case Some(assgn) => assgn.is_finished
1.150 + case None => false
1.151 + }
1.152 +
1.153 + def command_state(document: Document, command: Command): Command.State =
1.154 + {
1.155 + val assgn = the_assignment(document)
1.156 + require(assgn.is_finished)
1.157 + the_exec_state(assgn.join.getOrElse(command, fail))
1.158 }
1.159 }
1.160 }
1.161 @@ -226,28 +315,5 @@
1.162
1.163 class Document(
1.164 val id: Document.Version_ID,
1.165 - val nodes: Map[String, Document.Node],
1.166 - former_assignment: Map[Command, Command]) // FIXME !?
1.167 -{
1.168 - /* command state assignment */
1.169 + val nodes: Map[String, Document.Node])
1.170
1.171 - val assignment = Future.promise[Map[Command, Command]]
1.172 - def await_assignment { assignment.join }
1.173 -
1.174 - @volatile private var tmp_assignment = former_assignment
1.175 -
1.176 - def assign_execs(execs: List[(Command, Command)])
1.177 - {
1.178 - assignment.fulfill(tmp_assignment ++ execs)
1.179 - tmp_assignment = Map()
1.180 - }
1.181 -
1.182 - def current_state(cmd: Command): Command.State =
1.183 - {
1.184 - require(assignment.is_finished)
1.185 - (assignment.join).get(cmd) match {
1.186 - case Some(cmd_state) => cmd_state.current_state
1.187 - case None => new Command.State(cmd, Command.Status.UNDEFINED, 0, Nil, cmd.empty_markup)
1.188 - }
1.189 - }
1.190 -}