more robust;
authorwenzelm
Tue Jun 05 16:35:52 2018 +0200 (11 months ago)
changeset 68382b10ae73f0bab
parent 68381 2fd3a6d6ba2e
child 68383 93a42bd62ede
child 68399 0b71d08528f0
more robust;
src/Pure/PIDE/session.scala
     1.1 --- a/src/Pure/PIDE/session.scala	Tue Jun 05 16:12:26 2018 +0200
     1.2 +++ b/src/Pure/PIDE/session.scala	Tue Jun 05 16:35:52 2018 +0200
     1.3 @@ -318,7 +318,7 @@
     1.4      def flush(): Set[Document.Node.Name] =
     1.5        changed_nodes.change_result(nodes => (nodes, Set.empty))
     1.6  
     1.7 -    def shutdown() { delay.revoke() }
     1.8 +    def revoke() { delay.revoke() }
     1.9    }
    1.10  
    1.11  
    1.12 @@ -549,6 +549,7 @@
    1.13              prover.set(start_prover(manager.send(_)))
    1.14  
    1.15            case Stop =>
    1.16 +            consolidation.revoke()
    1.17              delay_prune.revoke()
    1.18              if (prover.defined) {
    1.19                protocol_handlers.exit()
    1.20 @@ -654,7 +655,6 @@
    1.21  
    1.22      change_parser.shutdown()
    1.23      change_buffer.shutdown()
    1.24 -    consolidation.shutdown()
    1.25      manager.shutdown()
    1.26      dispatcher.shutdown()
    1.27