tuned signature;
authorwenzelm
Mon, 07 Dec 2020 19:22:37 +0100
changeset 72845 60f56f623be2
parent 72844 240c8a0f6337
child 72846 a23e0964f3c3
tuned signature;
src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Dec 07 16:47:47 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Dec 07 19:22:37 2020 +0100
@@ -60,17 +60,6 @@
 
   /* base info and source dependencies */
 
-  object Base
-  {
-    def bootstrap(
-        session_directories: Map[JFile, String],
-        global_theories: Map[String, String]): Base =
-      Base(
-        session_directories = session_directories,
-        global_theories = global_theories,
-        overall_syntax = Thy_Header.bootstrap_syntax)
-  }
-
   sealed case class Base(
     pos: Position.T = Position.none,
     session_directories: Map[JFile, String] = Map.empty,
@@ -166,13 +155,8 @@
       }
     }
 
-    val bootstrap =
-      Sessions.Base.bootstrap(
-        sessions_structure.session_directories,
-        sessions_structure.global_theories)
-
     val session_bases =
-      (Map("" -> bootstrap) /: sessions_structure.imports_topological_order)({
+      (Map("" -> sessions_structure.bootstrap) /: sessions_structure.imports_topological_order)({
         case (session_bases, session_name) =>
           progress.expose_interrupt()
 
@@ -734,6 +718,12 @@
   {
     sessions_structure =>
 
+    def bootstrap: Base =
+      Base(
+        session_directories = session_directories,
+        global_theories = global_theories,
+        overall_syntax = Thy_Header.bootstrap_syntax)
+
     def dest_session_directories: List[(String, String)] =
       for ((file, session) <- session_directories.toList)
         yield (File.standard_path(file), session)