changeset 69255 | 800b1ce96fce |
parent 69035 | d75cd481f8d9 |
child 69458 | 5655af3ea5bd |
--- a/src/Pure/PIDE/headless.scala Wed Nov 07 14:06:43 2018 +0100 +++ b/src/Pure/PIDE/headless.scala Wed Nov 07 21:42:16 2018 +0100 @@ -263,7 +263,7 @@ else changed.nodes.iterator.filter(dep_theories_set).toSet val (nodes_status_changed, nodes_status1) = - st.nodes_status.update(resources.session_base, state, version, + st.nodes_status.update(resources, state, version, domain = Some(domain), trim = changed.assignment) if (nodes_status_delay >= Time.zero && nodes_status_changed) {