src/Tools/jEdit/src/jedit_resources.scala

 import org.gjt.sp.jedit.MiscUtilities
 import org.gjt.sp.jedit.{jEdit, View, Buffer}
 import org.gjt.sp.jedit.bufferio.BufferIORequest
 
 
-class JEdit_Resources(session_base: Sessions.Base) extends Resources(session_base)
+object JEdit_Resources
+{
+  def apply(options: Options): JEdit_Resources =
+  {
+    val (errs, base) = JEdit_Sessions.session_base(options)
+    new JEdit_Resources(errs, base)
+  }
+}
+
+class JEdit_Resources private(val session_errors: List[String], session_base: Sessions.Base)
+  extends Resources(session_base)
 {
   /* document node name */
 
   def known_file(path: String): Option[Document.Node.Name] =
     JEdit_Lib.check_file(path).flatMap(session_base.known.get_file(_, bootstrap = true))