tuned signature;

--- 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 */
 

--- 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)

--- 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)))
           }
         }
       }