prefer strict operation (despite 8edca3465758): there might be errors from all_known = true (ae09b9f5980b);

--- a/src/Tools/jEdit/src/plugin.scala	Sun Apr 23 14:15:09 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sun Apr 23 14:27:22 2017 +0200
@@ -73,11 +73,8 @@
     val options = this.options.value
     val session_name = JEdit_Sessions.session_name(options)
     val session_base =
-      try {
-        Sessions.session_base(
-          options, session_name, dirs = JEdit_Sessions.session_dirs(), all_known = true)
-      }
-      catch { case ERROR(_) => Sessions.Base.pure(options) }
+      Sessions.session_base(
+        options, session_name, dirs = JEdit_Sessions.session_dirs(), all_known = true)
 
     _resources = new JEdit_Resources(session_base.platform_path)
   }