more accurate management of dependencies: change of build_uuid causes output of HTML, but already existing/current HTML is not produced again;

--- 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 =

--- a/src/Pure/Thy/browser_info.scala	Thu Aug 25 16:05:33 2022 +0200
+++ b/src/Pure/Thy/browser_info.scala	Thu Aug 25 19:36:33 2022 +0200
@@ -78,6 +78,19 @@
     }
 
 
+    /* build_uuid */
+
+    val BUILD_UUID = "build_uuid"
+
+    def check_build_uuid(dir: Path, uuid: String): Boolean = {
+      val uuid0 = value(dir, BUILD_UUID)
+      uuid0.nonEmpty && uuid.nonEmpty && uuid0 == uuid
+    }
+
+    def set_build_uuid(dir: Path, uuid: String): Unit =
+      change(dir, BUILD_UUID)(_ => uuid)
+
+
     /* index */
 
     val INDEX = "index.json"
@@ -617,6 +630,8 @@
           context.contents("Theories", theories),
         root = Some(context.root_dir))
 
+    Meta_Data.set_build_uuid(session_dir, session.build_uuid)
+
     context.update_chapter(session_info.chapter, session_name, session_info.description)
   }
 
@@ -624,7 +639,7 @@
     browser_info: Config,
     store: Sessions.Store,
     deps: Sessions.Deps,
-    presentation_sessions: List[String],
+    sessions: List[String],
     progress: Progress = new Progress,
     verbose: Boolean = false
   ): Unit = {
@@ -632,19 +647,31 @@
     progress.echo("Presentation in " + root_dir)
 
     using(Export.open_database_context(store)) { database_context =>
-      val document_info = Document_Info.read(database_context, deps, presentation_sessions)
+      val context0 = context(deps.sessions_structure, elements1, root_dir = root_dir)
 
-      val context =
-        Browser_Info.context(deps.sessions_structure, elements1, root_dir = root_dir,
-          document_info = document_info)
+      val sessions1 =
+        deps.sessions_structure.build_requirements(sessions).filter { session_name =>
+          using(database_context.open_database(session_name)) { session_database =>
+            database_context.store.read_build(session_database.db, session_name) match {
+              case None => false
+              case Some(build) =>
+                val session_dir = context0.session_dir(session_name)
+                !Meta_Data.check_build_uuid(session_dir, build.uuid)
+            }
+          }
+        }
 
-      context.update_root()
+      val context1 =
+        context(deps.sessions_structure, elements1, root_dir = root_dir,
+          document_info = Document_Info.read(database_context, deps, sessions1))
+
+      context1.update_root()
 
       Par_List.map({ (session: String) =>
         using(database_context.open_session(deps.base_info(session))) { session_context =>
-          build_session(context, session_context, progress = progress, verbose = verbose)
+          build_session(context1, session_context, progress = progress, verbose = verbose)
         }
-      }, presentation_sessions)
+      }, sessions1)
     }
   }
 }