# HG changeset patch # User wenzelm # Date 1373368642 -7200 # Node ID f9a20c2c3b70c472cf3c15aa89cb6683f88117f0 # Parent 3261ee47bb9501609843849353b1d780e207af3e tuned protocol terminology; tuned signature; diff -r 3261ee47bb95 -r f9a20c2c3b70 src/Pure/PIDE/document.scala --- 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) diff -r 3261ee47bb95 -r f9a20c2c3b70 src/Pure/PIDE/markup.ML --- 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)]; diff -r 3261ee47bb95 -r f9a20c2c3b70 src/Pure/PIDE/markup.scala --- 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 diff -r 3261ee47bb95 -r f9a20c2c3b70 src/Pure/PIDE/protocol.ML --- 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 diff -r 3261ee47bb95 -r f9a20c2c3b70 src/Pure/PIDE/protocol.scala --- 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) diff -r 3261ee47bb95 -r f9a20c2c3b70 src/Pure/System/session.scala --- 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() }