src/Pure/PIDE/document_editor.scala

 
   def document_name: String = "document"
   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))
         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,
+          Meta_Info(name,
             SortedSet.from(selection),
             SHA1.fake_digest(sources),
             SHA1.fake_digest(log),
             SHA1.fake_digest(pdf))
         }

           "pdf" -> SHA1.digest(doc.pdf).toString)
       File.write(document_output(name).json, JSON.Format.pretty_print(json))
     }
   }
 
-  sealed case class Meta_Data(
+  sealed case class Meta_Info(
     name: String,
     selection: SortedSet[String],
     sources: SHA1.Digest,
     log: SHA1.Digest,
     pdf: SHA1.Digest

     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)
+    Meta_Info.write(selection, doc, name = name)
   }
 
   def view_document(name: String = document_name): Unit = {
     val path = document_output(name).pdf
     if (path.is_file) Isabelle_System.pdf_viewer(path)

     Isabelle_System.with_tmp_dir("document") { tmp_dir =>
       val engine = context.get_engine()
       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) {
         write_document(document_session.selection,
           engine.build_document(context, directory, verbose = true))