--- a/src/Tools/jEdit/src/jedit_resources.scala Wed Nov 01 13:06:01 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Wed Nov 01 15:32:07 2017 +0100
@@ -27,9 +27,10 @@
new JEdit_Resources(JEdit_Sessions.session_base_info(options))
}
-class JEdit_Resources private(session_base_info: Sessions.Base_Info)
+class JEdit_Resources private(val session_base_info: Sessions.Base_Info)
extends Resources(session_base_info.base.platform_path)
{
+ def session_name: String = session_base_info.session
def session_errors: List[String] = session_base_info.errors