diff -r b4a04fa01677 -r cec22f403c25 src/Pure/PIDE/document_info.scala --- a/src/Pure/PIDE/document_info.scala Thu Aug 25 16:05:33 2022 +0200 +++ b/src/Pure/PIDE/document_info.scala Thu Aug 25 19:36:33 2022 +0200 @@ -11,7 +11,11 @@ sealed case class Session( name: String, used_theories: List[String], - loaded_theories: Map[String, Theory]) + loaded_theories: Map[String, Theory], + build_uuid: String + ) { + if (build_uuid.isEmpty) error("Missing build_uuid for session " + quote(name)) + } object Theory { def apply( @@ -115,16 +119,24 @@ def read_session(session_name: String): Document_Info.Session = { val static_theories = deps(session_name).used_theories.map(_._1.theory) - val loaded_theories0 = { + val (thys, build_uuid) = { using(database_context.open_session(deps.base_info(session_name))) { session_context => - for { - theory_name <- static_theories - theory <- read_theory(session_context.theory(theory_name)) - } yield theory_name -> theory + val thys = + for { + theory_name <- static_theories + theory <- read_theory(session_context.theory(theory_name)) + } yield theory_name -> theory + val build_uuid = + (for { + db <- session_context.session_db(session_name) + build <- database_context.store.read_build(db, session_name) + } yield build.uuid).getOrElse("") + (thys, build_uuid) } - }.toMap + } + val loaded_theories0 = thys.toMap val used_theories = static_theories.filter(loaded_theories0.keySet) - Session(session_name, used_theories, loaded_theories0) + Session(session_name, used_theories, loaded_theories0, build_uuid) } val result0 =