clarified signature;
authorwenzelm
Sat, 06 Aug 2022 14:31:46 +0200
changeset 75777 ed32b5554ed3
parent 75776 72e77c8307ec
child 75778 d18c96b9b955
clarified signature;
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)
   }