more thorough assignment, e.g. when "purge" removes commands that were not assigned;
authorwenzelm
Sun May 19 18:10:45 2019 +0200 (4 months ago)
changeset 702843e17c3a5fd39
parent 70283 9ebbb53f4b50
child 70285 be248d734a5d
more thorough assignment, e.g. when "purge" removes commands that were not assigned;
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/session.scala
src/Tools/jEdit/src/pretty_text_area.scala
     1.1 --- a/src/Pure/PIDE/document.ML	Sun May 19 14:14:56 2019 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sun May 19 18:10:45 2019 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4    val remove_versions: Document_ID.version list -> state -> state
     1.5    val start_execution: state -> state
     1.6    val update: Document_ID.version -> Document_ID.version -> edit list -> string list -> state ->
     1.7 -    Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
     1.8 +    string list * Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
     1.9    val state: unit -> state
    1.10    val change_state: (state -> state) -> unit
    1.11  end;
    1.12 @@ -869,7 +869,7 @@
    1.13      val state' = state
    1.14        |> define_version new_version_id new_version assigned_nodes;
    1.15  
    1.16 -  in (removed, assign_result, state') end);
    1.17 +  in (Symtab.keys edited, removed, assign_result, state') end);
    1.18  
    1.19  end;
    1.20  
     2.1 --- a/src/Pure/PIDE/document.scala	Sun May 19 14:14:56 2019 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Sun May 19 18:10:45 2019 +0200
     2.3 @@ -651,7 +651,7 @@
     2.4      }
     2.5  
     2.6      val init: State =
     2.7 -      State().define_version(Version.init, Assignment.init).assign(Version.init.id, Nil)._2
     2.8 +      State().define_version(Version.init, Assignment.init).assign(Version.init.id, Nil, Nil)._2
     2.9    }
    2.10  
    2.11    final case class State private(
    2.12 @@ -768,10 +768,15 @@
    2.13            st <- command_states(version, command).iterator
    2.14          } yield st.exports)
    2.15  
    2.16 -    def assign(id: Document_ID.Version, update: Assign_Update): (List[Command], State) =
    2.17 +    def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update)
    2.18 +      : ((List[Node.Name], List[Command]), State) =
    2.19      {
    2.20        val version = the_version(id)
    2.21  
    2.22 +      val edited_set = edited.toSet
    2.23 +      val edited_nodes =
    2.24 +        (for { (name, _) <- version.nodes.iterator if edited_set(name.node) } yield name).toList
    2.25 +
    2.26        def upd(exec_id: Document_ID.Exec, st: Command.State)
    2.27            : Option[(Document_ID.Exec, Command.State)] =
    2.28          if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st)
    2.29 @@ -794,7 +799,7 @@
    2.30        val new_assignment = the_assignment(version).assign(update)
    2.31        val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
    2.32  
    2.33 -      (changed_commands, new_state)
    2.34 +      ((edited_nodes, changed_commands), new_state)
    2.35      }
    2.36  
    2.37      def is_assigned(version: Version): Boolean =
     3.1 --- a/src/Pure/PIDE/protocol.ML	Sun May 19 14:14:56 2019 +0200
     3.2 +++ b/src/Pure/PIDE/protocol.ML	Sun May 19 18:10:45 2019 +0200
     3.3 @@ -106,7 +106,7 @@
     3.4  
     3.5              val _ = Execution.discontinue ();
     3.6  
     3.7 -            val (removed, assign_update, state') =
     3.8 +            val (edited, removed, assign_update, state') =
     3.9                Document.update old_id new_id edits consolidate state;
    3.10              val _ =
    3.11                (singleton o Future.forks)
    3.12 @@ -117,12 +117,12 @@
    3.13  
    3.14              val _ =
    3.15                Output.protocol_message Markup.assign_update
    3.16 -                ((new_id, assign_update) |>
    3.17 +                ((new_id, edited, assign_update) |>
    3.18                    let
    3.19                      open XML.Encode;
    3.20                      fun encode_upd (a, bs) =
    3.21                        string (space_implode "," (map Value.print_int (a :: bs)));
    3.22 -                  in pair int (list encode_upd) end
    3.23 +                  in triple int (list string) (list encode_upd) end
    3.24                    |> YXML.chunks_of_body);
    3.25            in Document.start_execution state' end)));
    3.26  
     4.1 --- a/src/Pure/PIDE/protocol.scala	Sun May 19 14:14:56 2019 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.scala	Sun May 19 18:10:45 2019 +0200
     4.3 @@ -13,7 +13,9 @@
     4.4  
     4.5    object Assign_Update
     4.6    {
     4.7 -    def unapply(text: String): Option[(Document_ID.Version, Document.Assign_Update)] =
     4.8 +    def unapply(text: String)
     4.9 +      : Option[(Document_ID.Version, List[String], Document.Assign_Update)] =
    4.10 +    {
    4.11        try {
    4.12          import XML.Decode._
    4.13          def decode_upd(body: XML.Body): (Long, List[Long]) =
    4.14 @@ -21,12 +23,13 @@
    4.15              case a :: bs => (a, bs)
    4.16              case _ => throw new XML.XML_Body(body)
    4.17            }
    4.18 -        Some(pair(long, list(decode_upd _))(Symbol.decode_yxml(text)))
    4.19 +        Some(triple(long, list(string), list(decode_upd _))(Symbol.decode_yxml(text)))
    4.20        }
    4.21        catch {
    4.22          case ERROR(_) => None
    4.23          case _: XML.Error => None
    4.24        }
    4.25 +    }
    4.26    }
    4.27  
    4.28    object Removed
     5.1 --- a/src/Pure/PIDE/session.scala	Sun May 19 14:14:56 2019 +0200
     5.2 +++ b/src/Pure/PIDE/session.scala	Sun May 19 18:10:45 2019 +0200
     5.3 @@ -269,15 +269,19 @@
     5.4      }
     5.5      private val delay_flush = Standard_Thread.delay_first(output_delay) { flush() }
     5.6  
     5.7 -    def invoke(assign: Boolean, cmds: List[Command]): Unit = synchronized {
     5.8 -      assignment |= assign
     5.9 -      for (command <- cmds) {
    5.10 -        nodes += command.node_name
    5.11 -        command.blobs_names.foreach(nodes += _)
    5.12 -        commands += command
    5.13 +    def invoke(assign: Boolean, edited_nodes: List[Document.Node.Name], cmds: List[Command]): Unit =
    5.14 +      synchronized {
    5.15 +        assignment |= assign
    5.16 +        for (node <- edited_nodes) {
    5.17 +          nodes += node
    5.18 +        }
    5.19 +        for (command <- cmds) {
    5.20 +          nodes += command.node_name
    5.21 +          command.blobs_names.foreach(nodes += _)
    5.22 +          commands += command
    5.23 +        }
    5.24 +        delay_flush.invoke()
    5.25        }
    5.26 -      delay_flush.invoke()
    5.27 -    }
    5.28  
    5.29      def shutdown()
    5.30      {
    5.31 @@ -457,7 +461,7 @@
    5.32        {
    5.33          try {
    5.34            val st = global_state.change_result(f)
    5.35 -          change_buffer.invoke(false, List(st.command))
    5.36 +          change_buffer.invoke(false, Nil, List(st.command))
    5.37          }
    5.38          catch { case _: Document.State.Fail => bad_output() }
    5.39        }
    5.40 @@ -485,10 +489,11 @@
    5.41  
    5.42                case Markup.Assign_Update =>
    5.43                  msg.text match {
    5.44 -                  case Protocol.Assign_Update(id, update) =>
    5.45 +                  case Protocol.Assign_Update(id, edited, update) =>
    5.46                      try {
    5.47 -                      val cmds = global_state.change_result(_.assign(id, update))
    5.48 -                      change_buffer.invoke(true, cmds)
    5.49 +                      val (edited_nodes, cmds) =
    5.50 +                        global_state.change_result(_.assign(id, edited, update))
    5.51 +                      change_buffer.invoke(true, edited_nodes, cmds)
    5.52                        manager.send(Session.Change_Flush)
    5.53                      }
    5.54                      catch { case _: Document.State.Fail => bad_output() }
     6.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Sun May 19 14:14:56 2019 +0200
     6.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sun May 19 18:10:45 2019 +0200
     6.3 @@ -48,7 +48,7 @@
     6.4      val state1 =
     6.5        state0.continue_history(Future.value(version0), edits, Future.value(version1))
     6.6          .define_version(version1, state0.the_assignment(version0))
     6.7 -        .assign(version1.id, List(command.id -> List(Document_ID.make())))._2
     6.8 +        .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2
     6.9  
    6.10      (command.source, state1)
    6.11    }