--- 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)
--- 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))
--- 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,
--- 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)
}
}