evade clash with index.html (allow "Index.thy" even on case-insensitive file-systems);

--- a/src/Pure/Thy/presentation.scala	Fri Aug 19 23:58:44 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Sat Aug 20 00:24:04 2022 +0200
@@ -42,7 +42,11 @@
       root_dir + Path.explode(sessions_structure(session).chapter_session)
 
     def theory_html(theory: Document_Info.Theory): Path =
-      Path.explode(theory.print_short).html
+    {
+      val name1 = theory.print_short
+      val name2 = if (Word.lowercase(name1) == "index") theory.name else name1
+      Path.explode(name2).html
+    }
 
     def file_html(file: String): Path =
       Path.explode(file).squash.html

--- a/src/Pure/Thy/sessions.scala	Fri Aug 19 23:58:44 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Aug 20 00:24:04 2022 +0200
@@ -30,11 +30,8 @@
 
   def is_pure(name: String): Boolean = name == Thy_Header.PURE
 
-
   def exclude_session(name: String): Boolean = name == "" || name == DRAFT
-
-  def exclude_theory(name: String): Boolean =
-    name == root_name || name == "index" || name == "bib"
+  def exclude_theory(name: String): Boolean = name == root_name || name == "bib"
 
 
   /* ROOTS file format */