--- 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