clarified signature: more accurate session_base_info.sessions_structure;
authorwenzelm
Fri, 27 Mar 2020 12:13:39 +0100
changeset 71810 01d92325ddab
parent 71809 8a298184f3f9
child 71811 817e26a03198
clarified signature: more accurate session_base_info.sessions_structure;
src/Pure/PIDE/headless.scala
src/Pure/Thy/sessions.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 {
--- 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)
   }