# HG changeset patch # User wenzelm # Date 1661197026 -7200 # Node ID 787a203a20b6870af5ea7849fdbe946b7ed7cf3a # Parent 881871e0fa9ec062a71c4dc0c155cd3a9d7a4a35 more formal meta data, within ".browser_info"; update_chapter for each session when it is finished; diff -r 881871e0fa9e -r 787a203a20b6 src/Pure/Thy/browser_info.scala --- a/src/Pure/Thy/browser_info.scala Mon Aug 22 21:25:12 2022 +0200 +++ b/src/Pure/Thy/browser_info.scala Mon Aug 22 21:37:06 2022 +0200 @@ -36,6 +36,95 @@ } + /* meta data within the file-system */ + + object Meta_Data { + /* 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" + + "To avoid potential disaster, it has not been changed automatically.\n" + + "If this is the intended directory, please move/remove/empty it manually.") + } + } + + def init_directory(dir: Path): Path = { + check_directory(dir) + Isabelle_System.make_directory(dir + PATH) + dir + } + + + /* content */ + + def make_path(dir: Path, name: String): Path = + dir + PATH + Path.basic(name) + + def value(dir: Path, name: String): String = { + val path = make_path(dir, name) + if (path.is_file) File.read(path) else "" + } + + def change(dir: Path, name: String)(f: String => String): Unit = { + val path = make_path(dir, name) + val x = value(dir, name) + val y = + try { f(x) } + catch { case ERROR(msg) => error("Failed to change " + path.expand + ":\n" + msg)} + if (x != y) File.write(path, y) + } + + + /* index */ + + val INDEX = "index.json" + + object Item { + def parse(json: JSON.T): Item = { + def err(): Nothing = + error("Bad JSON object for item:\n" + JSON.Format.pretty_print(json)) + val obj = JSON.Object.unapply(json) getOrElse err() + + val name = JSON.string(obj, "name") getOrElse err() + val description = JSON.string(obj, "description") getOrElse "" + Item(name, description = Symbol.trim_blank_lines(description)) + } + } + + sealed case class Item(name: String, description: String = "") { + def json: JSON.T = JSON.Object("name" -> name, "description" -> description) + } + + object Index { + def parse(s: JSON.S, kind: String): Index = { + if (s.isEmpty) Index(kind, Nil) + else { + def err(): Nothing = error("Bad JSON object " + kind + " index:\n" + s) + + val json = JSON.parse(s) + val obj = JSON.Object.unapply(json) getOrElse err() + + val kind1 = JSON.string(obj, "kind") getOrElse err() + val items = JSON.list(obj, "items", x => Some(Item.parse(x))) getOrElse err() + if (kind == kind1) Index(kind, items) + else error("Expected index kind " + quote(kind) + " but found " + quote(kind1)) + } + } + } + + sealed case class Index(kind: String, items: List[Item]) { + def +(item: Item): Index = + Index(kind, (item :: items.filterNot(_.name == item.name)).sortBy(_.name)) + + def json: JSON.T = JSON.Object("kind" -> kind, "items" -> items.map(_.json)) + def print_json: JSON.S = JSON.Format.pretty_print(json) + } + } + + /* presentation elements */ sealed case class Elements( @@ -83,6 +172,9 @@ def session_dir(session: String): Path = root_dir + Path.explode(sessions_structure(session).chapter_session) + def chapter_dir(chapter: String): Path = + root_dir + Path.basic(chapter) + def theory_dir(theory: Document_Info.Theory): Path = session_dir(theory.dynamic_session) @@ -164,55 +256,40 @@ /* maintain presentation structure */ - private val sessions_path = Path.basic(".sessions") - - private def update_sessions_list( - chapter_dir: Path, - new_sessions: List[(String, String)] - ): List[(String, String)] = synchronized { - val path = chapter_dir + sessions_path - - val sessions0 = - if (path.is_file) { - import XML.Decode._ - list(pair(string, string))(Symbol.decode_yxml(File.read(path))) - } - else Nil - - val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList - - File.write(path, - { - import XML.Encode._ - YXML.string_of_body(list(pair(string, string))(sessions)) - }) + def update_chapter( + chapter: String, + session_name: String, + session_description: String + ): Unit = synchronized { + val dir = Meta_Data.init_directory(chapter_dir(chapter)) + 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 index = index0 + item + val sessions = index.items - sessions - } - - def update_chapter(chapter: String, new_sessions: List[(String, String)]): Unit = synchronized { - val chapter_dir = Isabelle_System.make_directory(root_dir + Path.basic(chapter)) - - val sessions = update_sessions_list(chapter_dir, new_sessions) + if (index != index0) { + val title = "Isabelle/" + chapter + " sessions" + HTML.write_document(dir, "index.html", + List(HTML.title(title + Isabelle_System.isabelle_heading())), + HTML.chapter(title) :: + (if (sessions.isEmpty) Nil + else + List(HTML.div("sessions", + List(HTML.description( + sessions.map(session => + (List(HTML.link(session.name + "/index.html", HTML.text(session.name))), + if (session.description.isEmpty) Nil + else HTML.break ::: List(HTML.pre(HTML.text(session.description)))))))))), + root = Some(root_dir)) + } - val title = "Isabelle/" + chapter + " sessions" - HTML.write_document(chapter_dir, "index.html", - List(HTML.title(title + Isabelle_System.isabelle_heading())), - HTML.chapter(title) :: - (if (sessions.isEmpty) Nil - else - List(HTML.div("sessions", - List(HTML.description( - sessions.map({ case (name, description) => - val descr = Symbol.trim_blank_lines(description) - (List(HTML.link(name + "/index.html", HTML.text(name))), - if (descr == "") Nil - else HTML.break ::: List(HTML.pre(HTML.text(descr)))) })))))), - root = Some(root_dir)) + index.print_json + } } def update_root(): Unit = synchronized { - Isabelle_System.make_directory(root_dir) + Meta_Data.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")) @@ -439,10 +516,11 @@ val session_name = session_context.session_name val session_info = session_context.sessions_structure(session_name) - val session_dir = - Isabelle_System.make_directory(context.session_dir(session_name)).expand + val session_dir = context.session_dir(session_name).expand + progress.echo("Presenting " + session_name + " in " + session_dir + " ...") - progress.echo("Presenting " + session_name + " in " + session_dir + " ...") + Meta_Data.init_directory(context.chapter_dir(session_info.chapter)) + Meta_Data.init_directory(session_dir) val session = context.document_info.the_session(session_name) @@ -538,6 +616,8 @@ context.head(title, List(HTML.par(document_links))) :: context.contents("Theories", theories), root = Some(context.root_dir)) + + context.update_chapter(session_info.chapter, session_name, session_info.description) } def build( @@ -560,14 +640,6 @@ context.update_root() - val chapter_infos = - presentation_sessions.map(deps.sessions_structure.apply).groupBy(_.chapter) - - for ((chapter, infos) <- chapter_infos.iterator) { - val entries = infos.map(info => (info.name, info.description)) - context.update_chapter(chapter, entries) - } - Par_List.map({ (session: String) => using(database_context.open_session(deps.base_info(session))) { session_context => build_session(context, session_context, progress = progress, verbose = verbose)