--- 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")
--- 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)
}
--- 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() }