--- a/src/Pure/PIDE/document.scala Tue Jul 09 13:16:10 2013 +0200
+++ b/src/Pure/PIDE/document.scala Tue Jul 09 13:17:22 2013 +0200
@@ -275,7 +275,8 @@
result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
}
- type Assign = List[(Document_ID.Command, List[Document_ID.Exec])] // exec state assignment
+ type Assign_Update =
+ List[(Document_ID.Command, List[Document_ID.Exec])] // update of exec state assignment
object State
{
@@ -293,21 +294,21 @@
def check_finished: Assignment = { require(is_finished); this }
def unfinished: Assignment = new Assignment(command_execs, false)
- def assign(
- add_command_execs: List[(Document_ID.Command, List[Document_ID.Exec])]): Assignment =
+ def assign(update: Assign_Update): Assignment =
{
require(!is_finished)
val command_execs1 =
- (command_execs /: add_command_execs) {
- case (res, (command_id, Nil)) => res - command_id
- case (res, assign) => res + assign
+ (command_execs /: update) {
+ case (res, (command_id, exec_ids)) =>
+ if (exec_ids.isEmpty) res - command_id
+ else res + (command_id -> exec_ids)
}
new Assignment(command_execs1, true)
}
}
val init: State =
- State().define_version(Version.init, Assignment.init).assign(Version.init.id)._2
+ State().define_version(Version.init, Assignment.init).assign(Version.init.id, Nil)._2
}
final case class State private(
@@ -346,8 +347,7 @@
def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail)
def the_read_state(id: Document_ID.Command): Command.State = commands.getOrElse(id, fail)
def the_exec_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
- def the_assignment(version: Version): State.Assignment =
- assignments.getOrElse(version.id, fail)
+ def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail)
def accumulate(id: Document_ID.Generic, message: XML.Elem): (Command.State, State) =
execs.get(id) match {
@@ -363,12 +363,12 @@
}
}
- def assign(id: Document_ID.Version, command_execs: Assign = Nil): (List[Command], State) =
+ def assign(id: Document_ID.Version, update: Assign_Update): (List[Command], State) =
{
val version = the_version(id)
val (changed_commands, new_execs) =
- ((Nil: List[Command], execs) /: command_execs) {
+ ((Nil: List[Command], execs) /: update) {
case ((commands1, execs1), (cmd_id, exec)) =>
val st1 = the_read_state(cmd_id)
val command = st1.command
@@ -384,7 +384,7 @@
}
(commands2, execs2)
}
- val new_assignment = the_assignment(version).assign(command_execs)
+ val new_assignment = the_assignment(version).assign(update)
val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
(changed_commands, new_state)
--- a/src/Pure/PIDE/markup.ML Tue Jul 09 13:16:10 2013 +0200
+++ b/src/Pure/PIDE/markup.ML Tue Jul 09 13:17:22 2013 +0200
@@ -140,7 +140,7 @@
val padding_line: Properties.entry
val dialogN: string val dialog: serial -> string -> T
val functionN: string
- val assign_execs: Properties.T
+ val assign_update: Properties.T
val removed_versions: Properties.T
val protocol_handler: string -> Properties.T
val invoke_scala: string -> string -> Properties.T
@@ -459,7 +459,7 @@
val functionN = "function"
-val assign_execs = [(functionN, "assign_execs")];
+val assign_update = [(functionN, "assign_update")];
val removed_versions = [(functionN, "removed_versions")];
fun protocol_handler name = [(functionN, "protocol_handler"), (nameN, name)];
--- a/src/Pure/PIDE/markup.scala Tue Jul 09 13:16:10 2013 +0200
+++ b/src/Pure/PIDE/markup.scala Tue Jul 09 13:17:22 2013 +0200
@@ -313,7 +313,7 @@
val FUNCTION = "function"
val Function = new Properties.String(FUNCTION)
- val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
+ val Assign_Update: Properties.T = List((FUNCTION, "assign_update"))
val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
object Protocol_Handler
--- a/src/Pure/PIDE/protocol.ML Tue Jul 09 13:16:10 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML Tue Jul 09 13:17:22 2013 +0200
@@ -50,7 +50,7 @@
val (assignment, state') = Document.update old_id new_id edits state;
val _ =
- Output.protocol_message Markup.assign_execs
+ Output.protocol_message Markup.assign_update
((new_id, assignment) |>
let open XML.Encode
in pair int (list (pair int (list int))) end
--- a/src/Pure/PIDE/protocol.scala Tue Jul 09 13:16:10 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala Tue Jul 09 13:17:22 2013 +0200
@@ -11,9 +11,9 @@
{
/* document editing */
- object Assign
+ object Assign_Update
{
- def unapply(text: String): Option[(Document_ID.Version, Document.Assign)] =
+ def unapply(text: String): Option[(Document_ID.Version, Document.Assign_Update)] =
try {
import XML.Decode._
val body = YXML.parse_body(text)
--- a/src/Pure/System/session.scala Tue Jul 09 13:16:10 2013 +0200
+++ b/src/Pure/System/session.scala Tue Jul 09 13:17:22 2013 +0200
@@ -396,11 +396,11 @@
val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
accumulate(state_id, prover.get.xml_cache.elem(message))
- case Markup.Assign_Execs =>
+ case Markup.Assign_Update =>
XML.content(output.body) match {
- case Protocol.Assign(id, assign) =>
+ case Protocol.Assign_Update(id, update) =>
try {
- val cmds = global_state >>> (_.assign(id, assign))
+ val cmds = global_state >>> (_.assign(id, update))
delay_commands_changed.invoke(true, cmds)
}
catch { case _: Document.State.Fail => bad_output() }