# HG changeset patch
# User wenzelm
# Date 1585307619 -3600
# Node ID 01d92325ddab512a4fddbcd3d9e70077741ebb0b
# Parent  8a298184f3f963956f834a576efeacbc92abe155
clarified signature: more accurate session_base_info.sessions_structure;

diff -r 8a298184f3f9 -r 01d92325ddab src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Fri Mar 27 12:03:20 2020 +0100
+++ b/src/Pure/PIDE/headless.scala	Fri Mar 27 12:13:39 2020 +0100
@@ -584,10 +584,8 @@
         }
       session.phase_changed += session_phase
 
-      val sessions_structure = Sessions.load_structure(options, dirs = session_base_info.dirs)
-
       progress.echo("Starting session " + session_base_info.session + " ...")
-      Isabelle_Process.start(session, options, sessions_structure,
+      Isabelle_Process.start(session, options, session_base_info.sessions_structure,
         logic = session_base_info.session, modes = print_mode)
 
       session_error.join match {
diff -r 8a298184f3f9 -r 01d92325ddab src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Mar 27 12:03:20 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Mar 27 12:13:39 2020 +0100
@@ -337,7 +337,6 @@
 
   sealed case class Base_Info(
     options: Options,
-    dirs: List[Path],
     session: String,
     sessions_structure: Structure,
     errors: List[String],
@@ -420,7 +419,7 @@
 
     val deps1 = Sessions.deps(selected_sessions1, progress = progress)
 
-    Base_Info(options, dirs, session1, full_sessions1, deps1.errors, deps1(session1), infos1)
+    Base_Info(options, session1, full_sessions1, deps1.errors, deps1(session1), infos1)
   }