removed unused var plugin;
authorwenzelm
Sat, 09 Jan 2010 21:31:59 +0100
changeset 348501c31074598e3
parent 34849 ca76b3978540
child 34851 77ac13833972
removed unused var plugin;
src/Tools/jEdit/src/jedit/plugin.scala
     1.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Sat Jan 09 18:25:48 2010 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Sat Jan 09 21:31:59 2010 +0100
     1.3 @@ -27,7 +27,6 @@
     1.4  {
     1.5    /* plugin instance */
     1.6  
     1.7 -  var plugin: Plugin = null
     1.8    var system: Isabelle_System = null
     1.9    var session: Session = null
    1.10  
    1.11 @@ -184,7 +183,6 @@
    1.12  
    1.13    override def start()
    1.14    {
    1.15 -    Isabelle.plugin = this
    1.16      Isabelle.system = new Isabelle_System
    1.17      Isabelle.system.install_fonts()
    1.18      Isabelle.session = new Session(Isabelle.system)  // FIXME dialog!?
    1.19 @@ -195,6 +193,5 @@
    1.20      Isabelle.session.stop()  // FIXME dialog!?
    1.21      Isabelle.session = null
    1.22      Isabelle.system = null
    1.23 -    Isabelle.plugin = null
    1.24    }
    1.25  }