changeset 34779 | d1040b77b189 |
parent 34777 | 91d6089cef88 |
child 34780 | d0ff1c3a91ea |
--- 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 }