tuned protocol terminology;
authorwenzelm
Tue Jul 09 13:17:22 2013 +0200 (2013-07-09)
changeset 52563f9a20c2c3b70
parent 52562 3261ee47bb95
child 52564 4e855c120f6a
tuned protocol terminology;
tuned signature;
src/Pure/PIDE/document.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/System/session.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Tue Jul 09 13:16:10 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Tue Jul 09 13:17:22 2013 +0200
     1.3 @@ -275,7 +275,8 @@
     1.4        result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
     1.5    }
     1.6  
     1.7 -  type Assign = List[(Document_ID.Command, List[Document_ID.Exec])]  // exec state assignment
     1.8 +  type Assign_Update =
     1.9 +    List[(Document_ID.Command, List[Document_ID.Exec])]  // update of exec state assignment
    1.10  
    1.11    object State
    1.12    {
    1.13 @@ -293,21 +294,21 @@
    1.14        def check_finished: Assignment = { require(is_finished); this }
    1.15        def unfinished: Assignment = new Assignment(command_execs, false)
    1.16  
    1.17 -      def assign(
    1.18 -        add_command_execs: List[(Document_ID.Command, List[Document_ID.Exec])]): Assignment =
    1.19 +      def assign(update: Assign_Update): Assignment =
    1.20        {
    1.21          require(!is_finished)
    1.22          val command_execs1 =
    1.23 -          (command_execs /: add_command_execs) {
    1.24 -            case (res, (command_id, Nil)) => res - command_id
    1.25 -            case (res, assign) => res + assign
    1.26 +          (command_execs /: update) {
    1.27 +            case (res, (command_id, exec_ids)) =>
    1.28 +              if (exec_ids.isEmpty) res - command_id
    1.29 +              else res + (command_id -> exec_ids)
    1.30            }
    1.31          new Assignment(command_execs1, true)
    1.32        }
    1.33      }
    1.34  
    1.35      val init: State =
    1.36 -      State().define_version(Version.init, Assignment.init).assign(Version.init.id)._2
    1.37 +      State().define_version(Version.init, Assignment.init).assign(Version.init.id, Nil)._2
    1.38    }
    1.39  
    1.40    final case class State private(
    1.41 @@ -346,8 +347,7 @@
    1.42      def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail)
    1.43      def the_read_state(id: Document_ID.Command): Command.State = commands.getOrElse(id, fail)
    1.44      def the_exec_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
    1.45 -    def the_assignment(version: Version): State.Assignment =
    1.46 -      assignments.getOrElse(version.id, fail)
    1.47 +    def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail)
    1.48  
    1.49      def accumulate(id: Document_ID.Generic, message: XML.Elem): (Command.State, State) =
    1.50        execs.get(id) match {
    1.51 @@ -363,12 +363,12 @@
    1.52            }
    1.53        }
    1.54  
    1.55 -    def assign(id: Document_ID.Version, command_execs: Assign = Nil): (List[Command], State) =
    1.56 +    def assign(id: Document_ID.Version, update: Assign_Update): (List[Command], State) =
    1.57      {
    1.58        val version = the_version(id)
    1.59  
    1.60        val (changed_commands, new_execs) =
    1.61 -        ((Nil: List[Command], execs) /: command_execs) {
    1.62 +        ((Nil: List[Command], execs) /: update) {
    1.63            case ((commands1, execs1), (cmd_id, exec)) =>
    1.64              val st1 = the_read_state(cmd_id)
    1.65              val command = st1.command
    1.66 @@ -384,7 +384,7 @@
    1.67                }
    1.68              (commands2, execs2)
    1.69          }
    1.70 -      val new_assignment = the_assignment(version).assign(command_execs)
    1.71 +      val new_assignment = the_assignment(version).assign(update)
    1.72        val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
    1.73  
    1.74        (changed_commands, new_state)
     2.1 --- a/src/Pure/PIDE/markup.ML	Tue Jul 09 13:16:10 2013 +0200
     2.2 +++ b/src/Pure/PIDE/markup.ML	Tue Jul 09 13:17:22 2013 +0200
     2.3 @@ -140,7 +140,7 @@
     2.4    val padding_line: Properties.entry
     2.5    val dialogN: string val dialog: serial -> string -> T
     2.6    val functionN: string
     2.7 -  val assign_execs: Properties.T
     2.8 +  val assign_update: Properties.T
     2.9    val removed_versions: Properties.T
    2.10    val protocol_handler: string -> Properties.T
    2.11    val invoke_scala: string -> string -> Properties.T
    2.12 @@ -459,7 +459,7 @@
    2.13  
    2.14  val functionN = "function"
    2.15  
    2.16 -val assign_execs = [(functionN, "assign_execs")];
    2.17 +val assign_update = [(functionN, "assign_update")];
    2.18  val removed_versions = [(functionN, "removed_versions")];
    2.19  
    2.20  fun protocol_handler name = [(functionN, "protocol_handler"), (nameN, name)];
     3.1 --- a/src/Pure/PIDE/markup.scala	Tue Jul 09 13:16:10 2013 +0200
     3.2 +++ b/src/Pure/PIDE/markup.scala	Tue Jul 09 13:17:22 2013 +0200
     3.3 @@ -313,7 +313,7 @@
     3.4    val FUNCTION = "function"
     3.5    val Function = new Properties.String(FUNCTION)
     3.6  
     3.7 -  val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
     3.8 +  val Assign_Update: Properties.T = List((FUNCTION, "assign_update"))
     3.9    val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
    3.10  
    3.11    object Protocol_Handler
     4.1 --- a/src/Pure/PIDE/protocol.ML	Tue Jul 09 13:16:10 2013 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.ML	Tue Jul 09 13:17:22 2013 +0200
     4.3 @@ -50,7 +50,7 @@
     4.4  
     4.5          val (assignment, state') = Document.update old_id new_id edits state;
     4.6          val _ =
     4.7 -          Output.protocol_message Markup.assign_execs
     4.8 +          Output.protocol_message Markup.assign_update
     4.9              ((new_id, assignment) |>
    4.10                let open XML.Encode
    4.11                in pair int (list (pair int (list int))) end
     5.1 --- a/src/Pure/PIDE/protocol.scala	Tue Jul 09 13:16:10 2013 +0200
     5.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Jul 09 13:17:22 2013 +0200
     5.3 @@ -11,9 +11,9 @@
     5.4  {
     5.5    /* document editing */
     5.6  
     5.7 -  object Assign
     5.8 +  object Assign_Update
     5.9    {
    5.10 -    def unapply(text: String): Option[(Document_ID.Version, Document.Assign)] =
    5.11 +    def unapply(text: String): Option[(Document_ID.Version, Document.Assign_Update)] =
    5.12        try {
    5.13          import XML.Decode._
    5.14          val body = YXML.parse_body(text)
     6.1 --- a/src/Pure/System/session.scala	Tue Jul 09 13:16:10 2013 +0200
     6.2 +++ b/src/Pure/System/session.scala	Tue Jul 09 13:17:22 2013 +0200
     6.3 @@ -396,11 +396,11 @@
     6.4                val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
     6.5                accumulate(state_id, prover.get.xml_cache.elem(message))
     6.6  
     6.7 -            case Markup.Assign_Execs =>
     6.8 +            case Markup.Assign_Update =>
     6.9                XML.content(output.body) match {
    6.10 -                case Protocol.Assign(id, assign) =>
    6.11 +                case Protocol.Assign_Update(id, update) =>
    6.12                    try {
    6.13 -                    val cmds = global_state >>> (_.assign(id, assign))
    6.14 +                    val cmds = global_state >>> (_.assign(id, update))
    6.15                      delay_commands_changed.invoke(true, cmds)
    6.16                    }
    6.17                    catch { case _: Document.State.Fail => bad_output() }