src/Pure/Thy/sessions.scala

 
             (other_name,
               List(
                 Info.make(
                   Chapter_Defs.empty,
+                  Options.init0(),
                   info.options,
                   augment_options = _ => Nil,
                   dir_selected = false,
                   dir = Path.explode("$ISABELLE_TMP_PREFIX"),
                   chapter = info.chapter,

   )
 
   object Info {
     def make(
       chapter_defs: Chapter_Defs,
+      options0: Options,
       options: Options,
       augment_options: String => List[Options.Spec],
       dir_selected: Boolean,
       dir: Path,
       chapter: String,

         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.session_prefs(defaults = options0)
 
         val theories =
           entry.theories.map({ case (opts, thys) =>
             (session_options ++ opts,
               thys.map({ case ((thy, pos), _) =>

 
         val meta_digest =
           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)
       }
       catch {
         case ERROR(msg) =>

     dir: Path,
     parent: Option[String],
     description: String,
     directories: List[Path],
     options: Options,
+    session_prefs: String,
     imports: List[String],
     theories: List[(Options, List[(String, Position.T)])],
     global_theories: List[String],
     document_theories: List[(String, Position.T)],
     document_files: List[(Path, Path)],

               case (defs2, entry: Chapter_Def) => defs2 + entry
               case (defs2, _) => defs2
             }
         }
 
+      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]
         for (root <- roots) {
           root.entries.foreach {
             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 _ =>
           }
           chapter = UNSORTED
         }

                   error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
                 case _ => global + (thy -> qualifier)
               }
           }
 
-      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],
     val build_graph: Graph[String, Info],
     val imports_graph: Graph[String, Info]

       def restrict(graph: Graph[String, Info]): Graph[String, Info] = {
         val sessions = graph.all_preds(selected(graph, sel)).filterNot(excluded)
         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))
 
     def selection_deps(