diff -r 7e5102e11c5e -r 945cee776e79 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Thu Nov 19 22:05:34 2020 +0100 +++ b/src/Pure/Thy/sessions.scala Fri Nov 20 12:00:08 2020 +0100 @@ -577,7 +577,8 @@ val meta_digest = SHA1.digest( (name, chapter, entry.parent, entry.directories, entry.options, entry.imports, - entry.theories_no_position, conditions, entry.document_theories, entry.document_files) + entry.theories_no_position, conditions, entry.document_theories_no_position, + entry.document_files) .toString) Info(name, chapter, dir_selected, entry.pos, entry.groups, session_path, @@ -877,6 +878,8 @@ { def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] = theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) }) + def document_theories_no_position: List[String] = + document_theories.map(_._1) } private object Parser extends Options.Parser