--- 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")