# HG changeset patch
# User wenzelm
# Date 1558282245 -7200
# Node ID 3e17c3a5fd39822fe5637b542ce9aca46c98469c
# Parent  9ebbb53f4b509406f01e6fa004618affa0f61779
more thorough assignment, e.g. when "purge" removes commands that were not assigned;

diff -r 9ebbb53f4b50 -r 3e17c3a5fd39 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sun May 19 14:14:56 2019 +0200
+++ b/src/Pure/PIDE/document.ML	Sun May 19 18:10:45 2019 +0200
@@ -25,7 +25,7 @@
   val remove_versions: Document_ID.version list -> state -> state
   val start_execution: state -> state
   val update: Document_ID.version -> Document_ID.version -> edit list -> string list -> state ->
-    Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
+    string list * Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
   val state: unit -> state
   val change_state: (state -> state) -> unit
 end;
@@ -869,7 +869,7 @@
     val state' = state
       |> define_version new_version_id new_version assigned_nodes;
 
-  in (removed, assign_result, state') end);
+  in (Symtab.keys edited, removed, assign_result, state') end);
 
 end;
 
diff -r 9ebbb53f4b50 -r 3e17c3a5fd39 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun May 19 14:14:56 2019 +0200
+++ b/src/Pure/PIDE/document.scala	Sun May 19 18:10:45 2019 +0200
@@ -651,7 +651,7 @@
     }
 
     val init: State =
-      State().define_version(Version.init, Assignment.init).assign(Version.init.id, Nil)._2
+      State().define_version(Version.init, Assignment.init).assign(Version.init.id, Nil, Nil)._2
   }
 
   final case class State private(
@@ -768,10 +768,15 @@
           st <- command_states(version, command).iterator
         } yield st.exports)
 
-    def assign(id: Document_ID.Version, update: Assign_Update): (List[Command], State) =
+    def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update)
+      : ((List[Node.Name], List[Command]), State) =
     {
       val version = the_version(id)
 
+      val edited_set = edited.toSet
+      val edited_nodes =
+        (for { (name, _) <- version.nodes.iterator if edited_set(name.node) } yield name).toList
+
       def upd(exec_id: Document_ID.Exec, st: Command.State)
           : Option[(Document_ID.Exec, Command.State)] =
         if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st)
@@ -794,7 +799,7 @@
       val new_assignment = the_assignment(version).assign(update)
       val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
 
-      (changed_commands, new_state)
+      ((edited_nodes, changed_commands), new_state)
     }
 
     def is_assigned(version: Version): Boolean =
diff -r 9ebbb53f4b50 -r 3e17c3a5fd39 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Sun May 19 14:14:56 2019 +0200
+++ b/src/Pure/PIDE/protocol.ML	Sun May 19 18:10:45 2019 +0200
@@ -106,7 +106,7 @@
 
             val _ = Execution.discontinue ();
 
-            val (removed, assign_update, state') =
+            val (edited, removed, assign_update, state') =
               Document.update old_id new_id edits consolidate state;
             val _ =
               (singleton o Future.forks)
@@ -117,12 +117,12 @@
 
             val _ =
               Output.protocol_message Markup.assign_update
-                ((new_id, assign_update) |>
+                ((new_id, edited, assign_update) |>
                   let
                     open XML.Encode;
                     fun encode_upd (a, bs) =
                       string (space_implode "," (map Value.print_int (a :: bs)));
-                  in pair int (list encode_upd) end
+                  in triple int (list string) (list encode_upd) end
                   |> YXML.chunks_of_body);
           in Document.start_execution state' end)));
 
diff -r 9ebbb53f4b50 -r 3e17c3a5fd39 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Sun May 19 14:14:56 2019 +0200
+++ b/src/Pure/PIDE/protocol.scala	Sun May 19 18:10:45 2019 +0200
@@ -13,7 +13,9 @@
 
   object Assign_Update
   {
-    def unapply(text: String): Option[(Document_ID.Version, Document.Assign_Update)] =
+    def unapply(text: String)
+      : Option[(Document_ID.Version, List[String], Document.Assign_Update)] =
+    {
       try {
         import XML.Decode._
         def decode_upd(body: XML.Body): (Long, List[Long]) =
@@ -21,12 +23,13 @@
             case a :: bs => (a, bs)
             case _ => throw new XML.XML_Body(body)
           }
-        Some(pair(long, list(decode_upd _))(Symbol.decode_yxml(text)))
+        Some(triple(long, list(string), list(decode_upd _))(Symbol.decode_yxml(text)))
       }
       catch {
         case ERROR(_) => None
         case _: XML.Error => None
       }
+    }
   }
 
   object Removed
diff -r 9ebbb53f4b50 -r 3e17c3a5fd39 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sun May 19 14:14:56 2019 +0200
+++ b/src/Pure/PIDE/session.scala	Sun May 19 18:10:45 2019 +0200
@@ -269,15 +269,19 @@
     }
     private val delay_flush = Standard_Thread.delay_first(output_delay) { flush() }
 
-    def invoke(assign: Boolean, cmds: List[Command]): Unit = synchronized {
-      assignment |= assign
-      for (command <- cmds) {
-        nodes += command.node_name
-        command.blobs_names.foreach(nodes += _)
-        commands += command
+    def invoke(assign: Boolean, edited_nodes: List[Document.Node.Name], cmds: List[Command]): Unit =
+      synchronized {
+        assignment |= assign
+        for (node <- edited_nodes) {
+          nodes += node
+        }
+        for (command <- cmds) {
+          nodes += command.node_name
+          command.blobs_names.foreach(nodes += _)
+          commands += command
+        }
+        delay_flush.invoke()
       }
-      delay_flush.invoke()
-    }
 
     def shutdown()
     {
@@ -457,7 +461,7 @@
       {
         try {
           val st = global_state.change_result(f)
-          change_buffer.invoke(false, List(st.command))
+          change_buffer.invoke(false, Nil, List(st.command))
         }
         catch { case _: Document.State.Fail => bad_output() }
       }
@@ -485,10 +489,11 @@
 
               case Markup.Assign_Update =>
                 msg.text match {
-                  case Protocol.Assign_Update(id, update) =>
+                  case Protocol.Assign_Update(id, edited, update) =>
                     try {
-                      val cmds = global_state.change_result(_.assign(id, update))
-                      change_buffer.invoke(true, cmds)
+                      val (edited_nodes, cmds) =
+                        global_state.change_result(_.assign(id, edited, update))
+                      change_buffer.invoke(true, edited_nodes, cmds)
                       manager.send(Session.Change_Flush)
                     }
                     catch { case _: Document.State.Fail => bad_output() }
diff -r 9ebbb53f4b50 -r 3e17c3a5fd39 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sun May 19 14:14:56 2019 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sun May 19 18:10:45 2019 +0200
@@ -48,7 +48,7 @@
     val state1 =
       state0.continue_history(Future.value(version0), edits, Future.value(version1))
         .define_version(version1, state0.the_assignment(version0))
-        .assign(version1.id, List(command.id -> List(Document_ID.make())))._2
+        .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2
 
     (command.source, state1)
   }