# HG changeset patch # User wenzelm # Date 1636112160 -3600 # Node ID decf8b66e2fbd5ca38df2ce3612a3fd599d2d4f7 # Parent 3c776254cd95336f36338e7a1e8aeaf193ba0690 more thorough update_global_index: overwrite old content; diff -r 3c776254cd95 -r decf8b66e2fb src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Fri Nov 05 12:33:27 2021 +0100 +++ b/src/Pure/Thy/presentation.scala Fri Nov 05 12:36:00 2021 +0100 @@ -301,15 +301,14 @@ else HTML.break ::: List(HTML.pre(HTML.text(descr)))) }))))))) } - def make_global_index(presentation_dir: Path): Unit = + def update_global_index(presentation_dir: Path): Unit = { - if (!(presentation_dir + Path.explode("index.html")).is_file) { - Isabelle_System.make_directory(presentation_dir) - Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"), - presentation_dir + Path.explode("isabelle.gif")) - val title = "The " + XML.text(Isabelle_System.isabelle_name()) + " Library" - File.write(presentation_dir + Path.explode("index.html"), - HTML.header + + Isabelle_System.make_directory(presentation_dir) + Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"), + presentation_dir + Path.explode("isabelle.gif")) + val title = "The " + XML.text(Isabelle_System.isabelle_name()) + " Library" + File.write(presentation_dir + Path.explode("index.html"), + HTML.header + """ """ + HTML.head_meta + """ @@ -337,7 +336,6 @@ """ """ + HTML.footer) - } } diff -r 3c776254cd95 -r decf8b66e2fb src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Fri Nov 05 12:33:27 2021 +0100 +++ b/src/Pure/Tools/build.scala Fri Nov 05 12:36:00 2021 +0100 @@ -521,7 +521,7 @@ for ((chapter, entries) <- browser_chapters) Presentation.update_chapter_index(presentation_dir, chapter, entries) - if (browser_chapters.nonEmpty) Presentation.make_global_index(presentation_dir) + if (browser_chapters.nonEmpty) Presentation.update_global_index(presentation_dir) } }