# HG changeset patch
# User wenzelm
# Date 1451936074 -3600
# Node ID c3c871b509d963383d3d0e698fab286d5585671d
# Parent  644a2eed86331c7bec00c0b0e028ca289aa3d4eb
stop dummy sessions as well;

diff -r 644a2eed8633 -r c3c871b509d9 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Mon Jan 04 20:23:14 2016 +0100
+++ b/src/Pure/Tools/debugger.scala	Mon Jan 04 20:34:34 2016 +0100
@@ -61,7 +61,10 @@
     output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
   {
     def set_session(new_session: Session): State =
+    {
+      session.stop()
       copy(session = new_session)
+    }
 
     def set_break(b: Boolean): State = copy(break = b)
 
diff -r 644a2eed8633 -r c3c871b509d9 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Jan 04 20:23:14 2016 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Jan 04 20:34:34 2016 +0100
@@ -398,6 +398,7 @@
       val resources =
         new JEdit_Resources(content.loaded_theories, content.known_theories, content.syntax)
 
+      PIDE.session.stop()
       PIDE.session = new Session(resources) {
         override def output_delay = PIDE.options.seconds("editor_output_delay")
         override def prune_delay = PIDE.options.seconds("editor_prune_delay")