clarified signature: more robust bootstrap base;
authorwenzelm
Wed, 01 Apr 2020 12:58:44 +0200
changeset 71642 77327455b00d
parent 71641 c1409b9c2b22
child 71643 43ba9fece20d
clarified signature: more robust bootstrap base;
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 =
             {