--- a/src/Tools/jEdit/src/plugin.scala Thu Jul 30 11:39:30 2015 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Thu Jul 30 14:02:19 2015 +0200
@@ -36,8 +36,7 @@
@volatile var startup_notified = false
@volatile var plugin: Plugin = null
- @volatile var session: Session =
- new Session(new JEdit_Resources(Set.empty, Map.empty, Outer_Syntax.empty))
+ @volatile var session: Session = new Session(JEdit_Resources.empty)
def options_changed() { plugin.options_changed() }
def deps_changed() { plugin.deps_changed() }