# HG changeset patch
# User wenzelm
# Date 1678718115 -3600
# Node ID 582a7db1da3727b4ffab2e3b928c67c2181c9d44
# Parent  af8ac22d97f07fc2a7bb8e90a9da9c28f7925f69
more accurate Sessions.Info.session_prefs: cover relative changes wrt. statically declared options;

diff -r af8ac22d97f0 -r 582a7db1da37 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Mar 13 15:09:08 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Mar 13 15:35:15 2023 +0100
@@ -258,7 +258,6 @@
               List(
                 Info.make(
                   Chapter_Defs.empty,
-                  Options.init0(),
                   info.options,
                   augment_options = _ => Nil,
                   dir_selected = false,
@@ -609,7 +608,6 @@
   object Info {
     def make(
       chapter_defs: Chapter_Defs,
-      options0: Options,
       options: Options,
       augment_options: String => List[Options.Spec],
       dir_selected: Boolean,
@@ -627,9 +625,10 @@
         val session_path = dir + Path.explode(entry.path)
         val directories = entry.directories.map(dir => session_path + Path.explode(dir))
 
-        val entry_options = entry.options ::: augment_options(name)
-        val session_options = options ++ entry_options
-        val session_prefs = options.make_prefs(defaults = options0, filter = _.session_content)
+        val session_options0 = options ++ entry.options
+        val session_options = session_options0 ++ augment_options(name)
+        val session_prefs =
+          session_options.make_prefs(defaults = session_options0, filter = _.session_content)
 
         val theories =
           entry.theories.map({ case (opts, thys) =>
@@ -664,7 +663,7 @@
 
         val meta_digest =
           SHA1.digest(
-            (name, chapter, entry.parent, entry.directories, entry_options, entry.imports,
+            (name, chapter, entry.parent, entry.directories, entry.options, entry.imports,
               entry.theories_no_position, conditions, entry.document_theories_no_position,
               entry.document_files, session_prefs)
             .toString)
@@ -824,8 +823,8 @@
             }
         }
 
-      val options0 = Options.init0()
-      val session_prefs = options.make_prefs(defaults = options0, filter = _.session_content)
+      val session_prefs =
+        options.make_prefs(defaults = Options.init0(), filter = _.session_content)
 
       val root_infos = {
         var chapter = UNSORTED
@@ -835,7 +834,7 @@
             case entry: Chapter_Entry => chapter = entry.name
             case entry: Session_Entry =>
               root_infos +=
-                Info.make(chapter_defs, options0, options, augment_options,
+                Info.make(chapter_defs, options, augment_options,
                   root.select, root.dir, chapter, entry)
             case _ =>
           }