changeset 70699 | 3eb30d80cee6 |
parent 70692 | 41b5e515c238 |
child 70716 | a8afe8eb3529 |
--- 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)