tuned;

--- a/src/Pure/Thy/sessions.scala	Thu Aug 31 16:35:09 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Aug 31 17:21:38 2017 +0200
@@ -307,10 +307,8 @@
     dirs: List[Path] = Nil,
     all_known: Boolean = false): Base =
   {
-    session_base_errors(options, session, dirs = dirs, all_known = all_known) match {
-      case (Nil, base) => base
-      case (errs, _) => error(cat_lines(errs))
-    }
+    val (errs, base) = session_base_errors(options, session, dirs = dirs, all_known = all_known)
+    if (errs.isEmpty) base else error(cat_lines(errs))
   }