--- a/src/Tools/jEdit/src/jedit_resources.scala Tue Oct 31 17:15:49 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Tue Oct 31 17:56:28 2017 +0100
@@ -24,15 +24,15 @@
object JEdit_Resources
{
def apply(options: Options): JEdit_Resources =
- {
- val (errs, base) = JEdit_Sessions.session_base(options)
- new JEdit_Resources(errs, base)
- }
+ new JEdit_Resources(JEdit_Sessions.session_base_info(options))
}
-class JEdit_Resources private(val session_errors: List[String], session_base: Sessions.Base)
- extends Resources(session_base)
+class JEdit_Resources private(session_base_info: Sessions.Base_Info)
+ extends Resources(session_base_info.base)
{
+ def session_errors: List[String] = session_base_info.errors
+
+
/* document node name */
def known_file(path: String): Option[Document.Node.Name] =