# HG changeset patch
# User wenzelm
# Date 1661005938 -7200
# Node ID b8ee1ef948c2ebbf19d15d9f002d6daec8e38342
# Parent  8fb3b3a106676e2b8e6d5896601ea2defa4cfaf8
more thorough checks of browser_info file conflicts;

diff -r 8fb3b3a10667 -r b8ee1ef948c2 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Sat Aug 20 14:55:21 2022 +0200
+++ b/src/Pure/General/path.scala	Sat Aug 20 16:32:18 2022 +0200
@@ -91,6 +91,8 @@
   val USER_HOME: Path = variable("USER_HOME")
   val ISABELLE_HOME: Path = variable("ISABELLE_HOME")
 
+  val index_html: Path = basic("index.html")
+
 
   /* explode */
 
@@ -158,6 +160,10 @@
       error(("Collision of file names due case-insensitivity:" :: collisions).mkString("\n  "))
     }
   }
+
+  def eq_case_insensitive(path1: Path, path2: Path): Boolean =
+    path1 == path2 ||
+    Word.lowercase(path1.expand.implode) == Word.lowercase(path2.expand.implode)
 }
 
 
diff -r 8fb3b3a10667 -r b8ee1ef948c2 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sat Aug 20 14:55:21 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Sat Aug 20 16:32:18 2022 +0200
@@ -43,9 +43,14 @@
 
     def theory_html(theory: Document_Info.Theory): Path =
     {
-      val name1 = theory.print_short
-      val name2 = if (Word.lowercase(name1) == "index") theory.name else name1
-      Path.explode(name2).html
+      def check(name: String): Option[Path] = {
+        val path = Path.explode(name).html
+        if (Path.eq_case_insensitive(path, Path.index_html)) None
+        else Some(path)
+      }
+      check(theory.print_short) orElse check(theory.name) getOrElse
+        error("Illegal global theory name " + quote(theory.name) +
+          " (conflict with " + Path.index_html + ")")
     }
 
     def file_html(file: String): Path =
@@ -466,6 +471,10 @@
       }
       yield {
         val doc_path = session_dir + doc.path.pdf
+        if (Path.eq_case_insensitive(doc.path.pdf, session_graph_path)) {
+          error("Illegal document variant " + quote(doc.name) +
+            " (conflict with " + session_graph_path + ")")
+        }
         if (verbose) progress.echo("Presenting document " + session_name + "/" + doc.name)
         if (session_info.document_echo) progress.echo("Document at " + doc_path)
         Bytes.write(doc_path, document.pdf)