# HG changeset patch
# User wenzelm
# Date 1568547721 -7200
# Node ID 3eb30d80cee62790a907ee30493b432d8c4f43f3
# Parent  93aa546ffbac597ff9d88447c78c65d380494bc6
tuned signature;

diff -r 93aa546ffbac -r 3eb30d80cee6 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Sun Sep 15 13:37:53 2019 +0200
+++ b/src/Pure/General/graph.scala	Sun Sep 15 13:42:01 2019 +0200
@@ -191,6 +191,8 @@
   def restrict(pred: Key => Boolean): Graph[Key, A] =
     (this /: iterator){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
 
+  def exclude(pred: Key => Boolean): Graph[Key, A] = restrict(name => !pred(name))
+
 
   /* edge operations */
 
diff -r 93aa546ffbac -r 3eb30d80cee6 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Sep 15 13:37:53 2019 +0200
+++ b/src/Pure/PIDE/document.scala	Sun Sep 15 13:42:01 2019 +0200
@@ -882,7 +882,7 @@
         blobs = blobs1,
         commands = commands1,
         execs = execs1,
-        commands_redirection = commands_redirection.restrict(commands1.isDefinedAt(_)),
+        commands_redirection = commands_redirection.restrict(commands1.keySet),
         assignments = assignments1,
         history = history.purge(versions1),
         removing_versions = false)
diff -r 93aa546ffbac -r 3eb30d80cee6 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Sun Sep 15 13:37:53 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Sun Sep 15 13:42:01 2019 +0200
@@ -74,10 +74,7 @@
           case current :: rest =>
             val dep_graph1 =
               if (rest.isEmpty) dep_graph
-              else {
-                val exclude = dep_graph.all_succs(rest).toSet
-                dep_graph.restrict(name => !exclude(name))
-              }
+              else dep_graph.exclude(dep_graph.all_succs(rest).toSet)
             dep_graph1.all_succs(List(current))
         }
 
@@ -184,7 +181,7 @@
           if (clean.isEmpty) (Nil, this)
           else {
             (dep_graph.topological_order.filter(clean),
-              copy(dep_graph = dep_graph.restrict(name => !clean(name))))
+              copy(dep_graph = dep_graph.exclude(clean)))
           }
         }
       }