# HG changeset patch
# User wenzelm
# Date 1675452217 -3600
# Node ID 9dc4d9ed886fbcbaeddcd047e6590744a205a5a1
# Parent  861777e58b7779c387a2b9e5ead8b85e11913181
maintain document_output meta data;

diff -r 861777e58b77 -r 9dc4d9ed886f src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Fri Feb 03 19:00:29 2023 +0100
+++ b/src/Pure/General/path.scala	Fri Feb 03 20:23:37 2023 +0100
@@ -239,6 +239,7 @@
   def gz: Path = ext("gz")
   def html: Path = ext("html")
   def jar: Path = ext("jar")
+  def json: Path = ext("json")
   def log: Path = ext("log")
   def orig: Path = ext("orig")
   def patch: Path = ext("patch")
diff -r 861777e58b77 -r 9dc4d9ed886f src/Pure/PIDE/document_editor.scala
--- a/src/Pure/PIDE/document_editor.scala	Fri Feb 03 19:00:29 2023 +0100
+++ b/src/Pure/PIDE/document_editor.scala	Fri Feb 03 20:23:37 2023 +0100
@@ -12,16 +12,73 @@
 
   def document_name: String = "document"
   def document_output_dir(): Path = Path.explode("$ISABELLE_HOME_USER/document_output")
-  def document_output(): Path = document_output_dir() + Path.basic(document_name)
+  def document_output(name: String): Path = document_output_dir() + Path.basic(name)
+
+  object Meta_Data {
+    def read(name: String = document_name): Option[Meta_Data] = {
+      val json_path = document_output(name).json
+      if (json_path.is_file) {
+        val json = JSON.parse(File.read(json_path))
+        for {
+          selection <- JSON.list(json, "selection", JSON.Value.String.unapply)
+          sources <- JSON.string(json, "sources")
+          log <- JSON.string(json, "log")
+          pdf <- JSON.string(json, "pdf")
+        } yield {
+          Meta_Data(name,
+            selection,
+            SHA1.fake_digest(sources),
+            SHA1.fake_digest(log),
+            SHA1.fake_digest(pdf))
+        }
+      }
+      else None
+    }
 
-  def write_document(doc: Document_Build.Document_Output): Unit = {
-    val output = document_output()
+    def write(
+      selection: Set[Document.Node.Name],
+      doc: Document_Build.Document_Output,
+      name: String = document_name
+    ): Unit = {
+      val json =
+        JSON.Object(
+          "selection" -> selection.toList.map(_.theory).sorted,
+          "sources" -> doc.sources.toString,
+          "log" -> SHA1.digest(doc.log).toString,
+          "pdf" -> SHA1.digest(doc.pdf).toString)
+      File.write(document_output(name).json, JSON.Format.pretty_print(json))
+    }
+  }
+
+  sealed case class Meta_Data(
+    name: String,
+    selection: List[String],
+    sources: SHA1.Digest,
+    log: SHA1.Digest,
+    pdf: SHA1.Digest
+  ) {
+    def check_files(): Boolean = {
+      val path = document_output(name)
+      path.log.is_file &&
+      path.pdf.is_file &&
+      log == SHA1.digest(File.read(path.log)) &&
+      pdf == SHA1.digest(path.pdf)
+    }
+  }
+
+  def write_document(
+    selection: Set[Document.Node.Name],
+    doc: Document_Build.Document_Output,
+    name: String = document_name
+  ): Unit = {
+    val output = document_output(name)
     File.write(output.log, doc.log)
     Bytes.write(output.pdf, doc.pdf)
+    Meta_Data.write(selection, doc, name = name)
   }
 
-  def view_document(): Unit = {
-    val path = document_output().pdf
+  def view_document(name: String = document_name): Unit = {
+    val path = document_output(name).pdf
     if (path.is_file) Isabelle_System.pdf_viewer(path)
   }
 
diff -r 861777e58b77 -r 9dc4d9ed886f src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Fri Feb 03 19:00:29 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Fri Feb 03 20:23:37 2023 +0100
@@ -221,7 +221,7 @@
       Isabelle_System.make_directory(Document_Editor.document_output_dir())
       val doc = context.build_document(document_session.get_variant, verbose = true)
 
-      Document_Editor.write_document(doc)
+      Document_Editor.write_document(document_session.selection, doc)
       Document_Editor.view_document()
     }
     finally { session_context.close() }