--- 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 +
"""
<head>
""" + HTML.head_meta + """
@@ -337,7 +336,6 @@
"""
</body>
""" + HTML.footer)
- }
}
--- 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)
}
}