# HG changeset patch
# User wenzelm
# Date 1263069119 -3600
# Node ID 1c31074598e38031cf394fc0e516fad56e2a8e03
# Parent  ca76b3978540665406b861b55d952d28b1cf56f4
removed unused var plugin;

diff -r ca76b3978540 -r 1c31074598e3 src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Sat Jan 09 18:25:48 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Sat Jan 09 21:31:59 2010 +0100
@@ -27,7 +27,6 @@
 {
   /* plugin instance */
 
-  var plugin: Plugin = null
   var system: Isabelle_System = null
   var session: Session = null
 
@@ -184,7 +183,6 @@
 
   override def start()
   {
-    Isabelle.plugin = this
     Isabelle.system = new Isabelle_System
     Isabelle.system.install_fonts()
     Isabelle.session = new Session(Isabelle.system)  // FIXME dialog!?
@@ -195,6 +193,5 @@
     Isabelle.session.stop()  // FIXME dialog!?
     Isabelle.session = null
     Isabelle.system = null
-    Isabelle.plugin = null
   }
 }