# HG changeset patch
# User wenzelm
# Date 1585738724 -7200
# Node ID 77327455b00d2c4e221dea917191be2ca4fa51c4
# Parent  c1409b9c2b221dd7069c783be26ff4685165ad09
clarified signature: more robust bootstrap base;

diff -r c1409b9c2b22 -r 77327455b00d src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Apr 01 12:57:19 2020 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Apr 01 12:58:44 2020 +0200
@@ -143,21 +143,19 @@
 
     val doc_names = Doc.doc_names()
 
+    val bootstrap =
+      Sessions.Base.bootstrap(
+        sessions_structure.session_directories,
+        sessions_structure.global_theories)
+
     val session_bases =
-      (Map.empty[String, Base] /: sessions_structure.imports_topological_order)({
+      (Map("" -> bootstrap) /: sessions_structure.imports_topological_order)({
         case (session_bases, session_name) =>
           progress.expose_interrupt()
 
           val info = sessions_structure(session_name)
           try {
-            val parent_base: Sessions.Base =
-              info.parent match {
-                case None =>
-                  Base.bootstrap(
-                    sessions_structure.session_directories,
-                    sessions_structure.global_theories)
-                case Some(parent) => session_bases(parent)
-              }
+            val parent_base = session_bases(info.parent.getOrElse(""))
 
             val imports_base: Sessions.Base =
             {