# 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 + """
-
-
-
-
-
- ![[Isabelle]](isabelle.gif) |
+ 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
-
-
-
- """ + 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
+ }
}
}