stop dummy sessions as well;
authorwenzelm
Mon, 04 Jan 2016 20:34:34 +0100
changeset 62051 c3c871b509d9
parent 62050 644a2eed8633
child 62052 8bcbf1c93119
stop dummy sessions as well;
src/Pure/Tools/debugger.scala
src/Tools/jEdit/src/plugin.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)
 
--- 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")