# HG changeset patch
# User wenzelm
# Date 1678534913 -3600
# Node ID 3b09ae9e40cba1b45fcbc0e1b153e3392f56ecba
# Parent  a45cce93529c3e07aa72cceb535e66263e72251a
clarified session prefs (or "options" within the database);

diff -r a45cce93529c -r 3b09ae9e40cb src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Sat Mar 11 11:51:19 2023 +0100
+++ b/src/Pure/System/options.scala	Sat Mar 11 12:41:53 2023 +0100
@@ -444,6 +444,9 @@
       .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString
   }
 
+  def session_prefs(defaults: Options = Options.init0()): String =
+    make_prefs(defaults = defaults, filter = _.session_content)
+
   def save_prefs(file: Path = Options.PREFS, defaults: Options = Options.init0()): Unit = {
     val prefs = make_prefs(defaults = defaults)
     Isabelle_System.make_directory(file.dir)
diff -r a45cce93529c -r 3b09ae9e40cb src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Mar 11 11:51:19 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Sat Mar 11 12:41:53 2023 +0100
@@ -258,6 +258,7 @@
               List(
                 Info.make(
                   Chapter_Defs.empty,
+                  Options.init0(),
                   info.options,
                   augment_options = _ => Nil,
                   dir_selected = false,
@@ -608,6 +609,7 @@
   object Info {
     def make(
       chapter_defs: Chapter_Defs,
+      options0: Options,
       options: Options,
       augment_options: String => List[Options.Spec],
       dir_selected: Boolean,
@@ -627,6 +629,7 @@
 
         val entry_options = entry.options ::: augment_options(name)
         val session_options = options ++ entry_options
+        val session_prefs = options.session_prefs(defaults = options0)
 
         val theories =
           entry.theories.map({ case (opts, thys) =>
@@ -663,14 +666,14 @@
           SHA1.digest(
             (name, chapter, entry.parent, entry.directories, entry_options, entry.imports,
               entry.theories_no_position, conditions, entry.document_theories_no_position,
-              entry.document_files)
+              entry.document_files, session_prefs)
             .toString)
 
         val chapter_groups = chapter_defs(chapter).groups
         val groups = chapter_groups ::: entry.groups.filterNot(chapter_groups.contains)
 
         Info(name, chapter, dir_selected, entry.pos, groups, session_path,
-          entry.parent, entry.description, directories, session_options,
+          entry.parent, entry.description, directories, session_options, session_prefs,
           entry.imports, theories, global_theories, entry.document_theories, document_files,
           export_files, entry.export_classpath, meta_digest)
       }
@@ -693,6 +696,7 @@
     description: String,
     directories: List[Path],
     options: Options,
+    session_prefs: String,
     imports: List[String],
     theories: List[(Options, List[(String, Position.T)])],
     global_theories: List[String],
@@ -820,6 +824,9 @@
             }
         }
 
+      val options0 = Options.init0()
+      val session_prefs = options.session_prefs(defaults = options0)
+
       val root_infos = {
         var chapter = UNSORTED
         val root_infos = new mutable.ListBuffer[Info]
@@ -828,7 +835,7 @@
             case entry: Chapter_Entry => chapter = entry.name
             case entry: Session_Entry =>
               root_infos +=
-                Info.make(chapter_defs, options, augment_options,
+                Info.make(chapter_defs, options0, options, augment_options,
                   root.select, root.dir, chapter, entry)
             case _ =>
           }
@@ -913,13 +920,14 @@
               }
           }
 
-      new Structure(chapter_defs, session_positions, session_directories,
+      new Structure(chapter_defs, session_prefs, session_positions, session_directories,
         global_theories, build_graph, imports_graph)
     }
   }
 
   final class Structure private[Sessions](
     chapter_defs: Chapter_Defs,
+    val session_prefs: String,
     val session_positions: List[(String, Position.T)],
     val session_directories: Map[JFile, String],
     val global_theories: Map[String, String],
@@ -1010,8 +1018,8 @@
         graph.restrict(graph.all_preds(sessions).toSet)
       }
 
-      new Structure(chapter_defs, session_positions, session_directories, global_theories,
-        restrict(build_graph), restrict(imports_graph))
+      new Structure(chapter_defs, session_prefs, session_positions, session_directories,
+        global_theories, restrict(build_graph), restrict(imports_graph))
     }
 
     def selection(session: String): Structure = selection(Selection.session(session))
diff -r a45cce93529c -r 3b09ae9e40cb src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sat Mar 11 11:51:19 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Sat Mar 11 12:41:53 2023 +0100
@@ -57,6 +57,7 @@
       name: String,
       deps: List[String],
       ancestors: List[String],
+      session_prefs: String,
       sources_shasum: SHA1.Shasum,
       timeout: Time,
       store: Sessions.Store,
@@ -64,7 +65,8 @@
     ): Session_Context = {
       def default: Session_Context =
         Session_Context(
-          name, deps, ancestors, sources_shasum, timeout, Time.zero, Bytes.empty, build_uuid)
+          name, deps, ancestors, session_prefs, sources_shasum, timeout,
+          Time.zero, Bytes.empty, build_uuid)
 
       store.try_open_database(name) match {
         case None => default
@@ -83,7 +85,8 @@
                 case _ => Time.zero
               }
             new Session_Context(
-              name, deps, ancestors, sources_shasum, timeout, elapsed, command_timings, build_uuid)
+              name, deps, ancestors, session_prefs, sources_shasum, timeout,
+              elapsed, command_timings, build_uuid)
           }
           catch {
             case ERROR(msg) => ignore_error(msg)
@@ -99,6 +102,7 @@
     name: String,
     deps: List[String],
     ancestors: List[String],
+    session_prefs: String,
     sources_shasum: SHA1.Shasum,
     timeout: Time,
     old_time: Time,
diff -r a45cce93529c -r 3b09ae9e40cb src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sat Mar 11 11:51:19 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sat Mar 11 12:41:53 2023 +0100
@@ -44,8 +44,8 @@
             val sources_shasum = build_deps.sources_shasum(name)
             val session_context =
               Build_Job.Session_Context.load(
-                build_uuid, name, deps, ancestors, sources_shasum, info.timeout, store,
-                progress = progress)
+                build_uuid, name, deps, ancestors, info.session_prefs, sources_shasum,
+                info.timeout, store, progress = progress)
             name -> session_context
           })
 
@@ -344,6 +344,7 @@
       val name = Generic.name.make_primary_key
       val deps = SQL.Column.string("deps")
       val ancestors = SQL.Column.string("ancestors")
+      val options = SQL.Column.string("options")
       val sources = SQL.Column.string("sources")
       val timeout = SQL.Column.long("timeout")
       val old_time = SQL.Column.long("old_time")
@@ -351,7 +352,8 @@
       val build_uuid = Generic.build_uuid
 
       val table = make_table("sessions",
-        List(name, deps, ancestors, sources, timeout, old_time, old_command_timings, build_uuid))
+        List(name, deps, ancestors, options, sources, timeout,
+          old_time, old_command_timings, build_uuid))
     }
 
     def read_sessions_domain(db: SQL.Database): Set[String] =
@@ -367,12 +369,13 @@
           val name = res.string(Sessions.name)
           val deps = split_lines(res.string(Sessions.deps))
           val ancestors = split_lines(res.string(Sessions.ancestors))
+          val options = res.string(Sessions.options)
           val sources_shasum = SHA1.fake_shasum(res.string(Sessions.sources))
           val timeout = Time.ms(res.long(Sessions.timeout))
           val old_time = Time.ms(res.long(Sessions.old_time))
           val old_command_timings_blob = res.bytes(Sessions.old_command_timings)
           val build_uuid = res.string(Sessions.build_uuid)
-          name -> Build_Job.Session_Context(name, deps, ancestors, sources_shasum,
+          name -> Build_Job.Session_Context(name, deps, ancestors, options, sources_shasum,
             timeout, old_time, old_command_timings_blob, build_uuid)
         }
       )
@@ -387,11 +390,12 @@
             stmt.string(1) = name
             stmt.string(2) = cat_lines(session.deps)
             stmt.string(3) = cat_lines(session.ancestors)
-            stmt.string(4) = session.sources_shasum.toString
-            stmt.long(5) = session.timeout.ms
-            stmt.long(6) = session.old_time.ms
-            stmt.bytes(7) = session.old_command_timings_blob
-            stmt.string(8) = session.build_uuid
+            stmt.string(4) = session.session_prefs
+            stmt.string(5) = session.sources_shasum.toString
+            stmt.long(6) = session.timeout.ms
+            stmt.long(7) = session.old_time.ms
+            stmt.bytes(8) = session.old_command_timings_blob
+            stmt.string(9) = session.build_uuid
           })
       }
 
@@ -923,7 +927,7 @@
   final def start_build(): Unit = synchronized_database {
     for (db <- _database) {
       Build_Process.Data.start_build(db, build_uuid, build_context.ml_platform,
-        store.options.make_prefs(Options.init0(), filter = _.session_content))
+        build_context.sessions_structure.session_prefs)
     }
   }