tuned;
authorwenzelm
Tue, 13 Jun 2017 20:19:25 +0200
changeset 66083 dcc685d5c3f7
parent 66082 2d12a730a380
child 66084 7f8eeff20f7a
tuned;
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Jun 13 20:16:39 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Jun 13 20:19:25 2017 +0200
@@ -16,7 +16,7 @@
 import org.gjt.sp.jedit.browser.VFSBrowser
 
 
-object JEdit_Editor extends Editor[View]
+class JEdit_Editor extends Editor[View]
 {
   /* session */
 
--- a/src/Tools/jEdit/src/plugin.scala	Tue Jun 13 20:16:39 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Jun 13 20:19:25 2017 +0200
@@ -56,7 +56,7 @@
   def resources: JEdit_Resources = plugin.resources
   def session: Session = plugin.session
 
-  val editor = JEdit_Editor
+  object editor extends JEdit_Editor
 }
 
 class Plugin extends EBPlugin