# HG changeset patch # User wenzelm # Date 1369232032 -7200 # Node ID 2d2b049429f389b9598140b87bef65e406fb7406 # Parent 3610ae73cfdbd1fa31431a3876cb35de7979f663 stop protocol handlers as well; diff -r 3610ae73cfdb -r 2d2b049429f3 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Wed May 22 16:01:08 2013 +0200 +++ b/src/Pure/System/session.scala Wed May 22 16:13:52 2013 +0200 @@ -98,6 +98,12 @@ } case _ => false } + + def stop(prover: Prover): Protocol_Handlers = + { + for ((_, handler) <- handlers) handler.stop(prover) + new Protocol_Handlers() + } } } @@ -462,6 +468,7 @@ case Stop => if (phase == Session.Ready) { + protocol_handlers = protocol_handlers.stop(prover.get) global_state >> (_ => Document.State.init) // FIXME event bus!? phase = Session.Shutdown prover.get.terminate