# HG changeset patch
# User wenzelm
# Date 1260567655 -3600
# Node ID d1040b77b189f31d27078c9abed79882a83ff629
# Parent  8eccd35e975e054a346105a2084e8016f1b4b40b
proper uninstall;

diff -r 8eccd35e975e -r d1040b77b189 src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Fri Dec 11 22:25:28 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Fri Dec 11 22:40:55 2009 +0100
@@ -94,7 +94,8 @@
   private def uninstall(view: View)
   {
     val buffer = view.getBuffer
-    mapping(buffer).deactivate
+    Isabelle.session.stop()
+    mapping(buffer).deactivate()
     mapping -= buffer
   }