# HG changeset patch # User wenzelm # Date 1661543331 -7200 # Node ID 46c6f649a943223f2fb4c0c64159296d2a00381d # Parent ca73ced9e630872e4e7b9261ea87bcb2a0bd0c26 produce root index based on sessions_structure.chapter_defs; disregard lib/html/library_index_content.template (NB: still needed for Isabelle website); diff -r ca73ced9e630 -r 46c6f649a943 src/Pure/Thy/browser_info.scala --- a/src/Pure/Thy/browser_info.scala Fri Aug 26 21:35:48 2022 +0200 +++ b/src/Pure/Thy/browser_info.scala Fri Aug 26 21:48:51 2022 +0200 @@ -311,36 +311,40 @@ HTML.init_fonts(root_dir) Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"), root_dir + Path.explode("isabelle.gif")) - val title = "The " + XML.text(Isabelle_System.isabelle_name()) + " Library" - File.write(root_dir + Path.explode("index.html"), - HTML.header + -""" - - """ + HTML.head_meta + """ - """ + title + """ - - -
- - - + Meta_Data.change(root_dir, Meta_Data.INDEX) { text => + val index0 = Meta_Data.Index.parse(text, "root") + val index = { + val items1 = + for (entry <- sessions_structure.chapter_defs.list) + yield Meta_Data.Item(entry.name, description = entry.description) + val items2 = + (for { + (name, _) <- sessions_structure.chapters.iterator + if !items1.exists(_.name == name) + } yield Meta_Data.Item(name)).toList + (items1 ::: items2).foldLeft(index0)(_ + _) + } + val chapters = index.items - - -
[Isabelle] - - - - -
""" + title + """
-
-
-
-""" + File.read(Path.explode("~~/lib/html/library_index_content.template")) + -""" - -""" + HTML.footer) + if (index != index0) { + val title = "The " + XML.text(Isabelle_System.isabelle_name()) + " Library" + HTML.write_document(root_dir, "index.html", + List(HTML.title(title + Isabelle_System.isabelle_heading())), + HTML.chapter(title) :: + (if (chapters.isEmpty) Nil + else + List(HTML.div("sessions", + List(HTML.description( + chapters.map(chapter => + (List(HTML.link(chapter.name + "/index.html", HTML.text(chapter.name))), + if (chapter.description.isEmpty) Nil + else HTML.break ::: List(HTML.pre(HTML.text(chapter.description)))))))))), + root = Some(root_dir)) + } + + index.print_json + } } }