src/Tools/jEdit/src/jedit/Plugin.scala
changeset 34732 1b0cfb4812d9
parent 34724 b1079c3ba1da
child 34751 6ed1b3701459
equal deleted inserted replaced
34731:c0cb6bd10eec 34732:1b0cfb4812d9
   162   override def stop()
   162   override def stop()
   163   {
   163   {
   164     // TODO: proper cleanup
   164     // TODO: proper cleanup
   165     Isabelle.system = null
   165     Isabelle.system = null
   166     Isabelle.plugin = null
   166     Isabelle.plugin = null
   167     scala.actors.Scheduler.shutdown()
       
   168   }
   167   }
   169 }
   168 }