# 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) } } }