clarified signature;

--- a/src/Pure/PIDE/headless.scala	Fri Mar 27 12:46:56 2020 +0100
+++ b/src/Pure/PIDE/headless.scala	Fri Mar 27 13:02:56 2020 +0100
@@ -396,8 +396,8 @@
 
   object Resources
   {
-    def apply(base_info: Sessions.Base_Info, log: Logger = No_Logger): Resources =
-      new Resources(base_info, log = log)
+    def apply(options: Options, base_info: Sessions.Base_Info, log: Logger = No_Logger): Resources =
+      new Resources(options, base_info, log = log)
 
     def make(
       options: Options,
@@ -410,7 +410,7 @@
       val base_info =
         Sessions.base_info(options, session_name, dirs = session_dirs,
           include_sessions = include_sessions, progress = progress)
-      apply(base_info, log = log)
+      apply(options, base_info, log = log)
     }
 
     final class Theory private[Headless](
@@ -554,6 +554,7 @@
   }
 
   class Resources private[Headless](
+      val options: Options,
       val session_base_info: Sessions.Base_Info,
       log: Logger = No_Logger)
     extends isabelle.Resources(
@@ -561,8 +562,6 @@
   {
     resources =>
 
-    def options: Options = session_base_info.options
-
 
     /* session */
 

--- a/src/Pure/Thy/sessions.scala	Fri Mar 27 12:46:56 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Mar 27 13:02:56 2020 +0100
@@ -336,7 +336,6 @@
   /* base info */
 
   sealed case class Base_Info(
-    options: Options,
     session: String,
     sessions_structure: Structure,
     errors: List[String],
@@ -419,7 +418,7 @@
 
     val deps1 = Sessions.deps(selected_sessions1, progress = progress)
 
-    Base_Info(options, session1, full_sessions1, deps1.errors, deps1(session1), infos1)
+    Base_Info(session1, full_sessions1, deps1.errors, deps1(session1), infos1)
   }
 
 

--- a/src/Pure/Tools/server_commands.scala	Fri Mar 27 12:46:56 2020 +0100
+++ b/src/Pure/Tools/server_commands.scala	Fri Mar 27 13:02:56 2020 +0100
@@ -46,7 +46,7 @@
       }
 
     def command(args: Args, progress: Progress = No_Progress)
-      : (JSON.Object.T, Build.Results, Sessions.Base_Info) =
+      : (JSON.Object.T, Build.Results, Options, Sessions.Base_Info) =
     {
       val options = Options.init(prefs = args.preferences, opts = args.options)
       val dirs = args.dirs.map(Path.explode(_))
@@ -85,7 +85,7 @@
                   "timing" -> result.timing.json)
               }))
 
-      if (results.ok) (results_json, results, base_info)
+      if (results.ok) (results_json, results, options, base_info)
       else throw new Server.Error("Session build failed: return code " + results.rc, results_json)
     }
   }
@@ -106,11 +106,11 @@
     def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger)
       : (JSON.Object.T, (UUID.T, Headless.Session)) =
     {
-      val base_info =
-        try { Session_Build.command(args.build, progress = progress)._3 }
+      val (_, _, options, base_info) =
+        try { Session_Build.command(args.build, progress = progress) }
         catch { case exn: Server.Error => error(exn.message) }
 
-      val resources = Headless.Resources(base_info, log = log)
+      val resources = Headless.Resources(options, base_info, log = log)
 
       val session = resources.start_session(print_mode = args.print_mode, progress = progress)