# HG changeset patch
# User wenzelm
# Date 1675675212 -3600
# Node ID 064566bc1f35f3f5910ff26c5bc20f28ccff89b7
# Parent  2cf7a61e4a73b8a0b3a4230d8cb3adf0ab4ad1e7
clarified signature: follow terminology of isabelle.Sessions and isabelle.Build;

diff -r 2cf7a61e4a73 -r 064566bc1f35 src/Pure/PIDE/document_editor.scala
--- a/src/Pure/PIDE/document_editor.scala	Mon Feb 06 10:03:55 2023 +0100
+++ b/src/Pure/PIDE/document_editor.scala	Mon Feb 06 10:20:12 2023 +0100
@@ -17,8 +17,8 @@
   def document_output_dir(): Path = Path.explode("$ISABELLE_HOME_USER/document_output")
   def document_output(name: String): Path = document_output_dir() + Path.basic(name)
 
-  object Meta_Data {
-    def read(name: String = document_name): Option[Meta_Data] = {
+  object Meta_Info {
+    def read(name: String = document_name): Option[Meta_Info] = {
       val json_path = document_output(name).json
       if (json_path.is_file) {
         val json = JSON.parse(File.read(json_path))
@@ -28,7 +28,7 @@
           log <- JSON.string(json, "log")
           pdf <- JSON.string(json, "pdf")
         } yield {
-          Meta_Data(name,
+          Meta_Info(name,
             SortedSet.from(selection),
             SHA1.fake_digest(sources),
             SHA1.fake_digest(log),
@@ -53,7 +53,7 @@
     }
   }
 
-  sealed case class Meta_Data(
+  sealed case class Meta_Info(
     name: String,
     selection: SortedSet[String],
     sources: SHA1.Digest,
@@ -77,7 +77,7 @@
     val output = document_output(name)
     File.write(output.log, doc.log)
     Bytes.write(output.pdf, doc.pdf)
-    Meta_Data.write(selection, doc, name = name)
+    Meta_Info.write(selection, doc, name = name)
   }
 
   def view_document(name: String = document_name): Unit = {
@@ -171,9 +171,9 @@
       val variant = document_session.get_variant
       val directory = engine.prepare_directory(context, tmp_dir, variant, verbose = true)
       val ok =
-        Meta_Data.read() match {
-          case Some(meta_data) =>
-            meta_data.check_files() && meta_data.sources == directory.sources
+        Meta_Info.read() match {
+          case Some(meta_info) =>
+            meta_info.check_files() && meta_info.sources == directory.sources
           case None => false
         }
       if (!ok) {
diff -r 2cf7a61e4a73 -r 064566bc1f35 src/Pure/Thy/browser_info.scala
--- a/src/Pure/Thy/browser_info.scala	Mon Feb 06 10:03:55 2023 +0100
+++ b/src/Pure/Thy/browser_info.scala	Mon Feb 06 10:20:12 2023 +0100
@@ -36,16 +36,16 @@
   }
 
 
-  /* meta data within the file-system */
+  /* meta info within the file-system */
 
-  object Meta_Data {
+  object Meta_Info {
     /* directory */
 
     val PATH: Path = Path.explode(".browser_info")
 
     def check_directory(dir: Path): Unit = {
       if (dir.is_dir && !(dir + PATH).is_dir && File.read_dir(dir).nonEmpty) {
-        error("Existing content in " + dir.expand + " lacks " + PATH + " meta data.\n" +
+        error("Existing content in " + dir.expand + " lacks " + PATH + " meta info.\n" +
           "To avoid potential disaster, it has not been changed automatically.\n" +
           "If this is the intended directory, please move/remove/empty it manually.")
       }
@@ -284,10 +284,10 @@
     /* maintain presentation structure */
 
     def update_chapter(session_name: String, session_description: String): Unit = synchronized {
-      val dir = Meta_Data.init_directory(chapter_dir(session_name))
-      Meta_Data.change(dir, Meta_Data.INDEX) { text =>
-        val index0 = Meta_Data.Index.parse(text, "chapter")
-        val item = Meta_Data.Item(session_name, description = session_description)
+      val dir = Meta_Info.init_directory(chapter_dir(session_name))
+      Meta_Info.change(dir, Meta_Info.INDEX) { text =>
+        val index0 = Meta_Info.Index.parse(text, "chapter")
+        val item = Meta_Info.Item(session_name, description = session_description)
         val index = index0 + item
 
         if (index != index0) {
@@ -311,17 +311,17 @@
     }
 
     def update_root(): Unit = synchronized {
-      Meta_Data.init_directory(root_dir)
+      Meta_Info.init_directory(root_dir)
       HTML.init_fonts(root_dir)
       Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"),
         root_dir + Path.explode("isabelle.gif"))
 
-      Meta_Data.change(root_dir, Meta_Data.INDEX) { text =>
-        val index0 = Meta_Data.Index.parse(text, "root")
+      Meta_Info.change(root_dir, Meta_Info.INDEX) { text =>
+        val index0 = Meta_Info.Index.parse(text, "root")
         val index = {
           val items1 =
             sessions_structure.known_chapters
-              .map(ch => Meta_Data.Item(ch.name, description = ch.description))
+              .map(ch => Meta_Info.Item(ch.name, description = ch.description))
           val items2 = index0.items.filterNot(item => items1.exists(_.name == item.name))
           index0.copy(items = items1 ::: items2)
         }
@@ -559,8 +559,8 @@
     val session_dir = context.session_dir(session_name).expand
     progress.echo("Presenting " + session_name + " in " + session_dir + " ...")
 
-    Meta_Data.init_directory(context.chapter_dir(session_name))
-    Meta_Data.clean_directory(session_dir)
+    Meta_Info.init_directory(context.chapter_dir(session_name))
+    Meta_Info.clean_directory(session_dir)
 
     val session = context.document_info.the_session(session_name)
 
@@ -662,7 +662,7 @@
           context.contents("Theories", theories),
         root = Some(context.root_dir))
 
-    Meta_Data.set_build_uuid(session_dir, session.build_uuid)
+    Meta_Info.set_build_uuid(session_dir, session.build_uuid)
 
     context.update_chapter(session_name, session_info.description)
   }
@@ -688,7 +688,7 @@
               case None => false
               case Some(build) =>
                 val session_dir = context0.session_dir(session_name)
-                !Meta_Data.check_build_uuid(session_dir, build.uuid)
+                !Meta_Info.check_build_uuid(session_dir, build.uuid)
             }
           }
         }