# HG changeset patch
# User wenzelm
# Date 1659789106 -7200
# Node ID ed32b5554ed3a3c3d736852ffd33b3f75b163987
# Parent  72e77c8307ecb4d8dc6ccf25c5a2fbc6726aeef5
clarified signature;

diff -r 72e77c8307ec -r ed32b5554ed3 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Aug 06 14:11:19 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Aug 06 14:31:46 2022 +0200
@@ -128,7 +128,7 @@
       }
 
     def base_info(session: String): Base_Info =
-      Base_Info(sessions_structure, errors, apply(session), Nil)
+      Base_Info(base = apply(session), sessions_structure = sessions_structure, errors = errors)
   }
 
   def deps(sessions_structure: Structure,
@@ -369,15 +369,18 @@
   /* base info */
 
   sealed case class Base_Info(
-    sessions_structure: Structure,
-    errors: List[String],
     base: Base,
-    infos: List[Info]
+    sessions_structure: Structure = Structure.empty,
+    errors: List[String] = Nil,
+    infos: List[Info] = Nil
   ) {
     def check: Base_Info = if (errors.isEmpty) this else error(cat_lines(errors))
     def session: String = base.session_name
   }
 
+  def base_info_empty(session: String): Base_Info =
+    Base_Info(Base(session_name = session))
+
   def base_info(options: Options,
     session: String,
     progress: Progress = new Progress,
@@ -453,7 +456,8 @@
 
     val deps1 = Sessions.deps(selected_sessions1, progress = progress)
 
-    Base_Info(full_sessions1, deps1.errors, deps1(session1), infos1)
+    Base_Info(deps1(session1), sessions_structure = full_sessions1,
+      errors = deps1.errors, infos = infos1)
   }