more sanity checks;

--- a/src/Pure/General/path.scala	Tue Mar 12 15:34:33 2019 +0100
+++ b/src/Pure/General/path.scala	Wed Mar 13 13:46:16 2019 +0100
@@ -130,6 +130,23 @@
 
   def is_reserved(name: String): Boolean =
     Long_Name.explode(name).exists(a => reserved_windows.contains(Word.uppercase(a)))
+
+
+  /* case-insensitive names */
+
+  def check_case_insensitive(paths: List[Path])
+  {
+    val table =
+      (Multi_Map.empty[String, String] /: paths)({ case (tab, path) =>
+        val name = path.expand.implode
+        tab.insert(Word.lowercase(name), name)
+      })
+    val collisions =
+      (for { (_, coll) <- table.iterator_list if coll.length > 1 } yield coll).toList.flatten
+    if (collisions.nonEmpty) {
+      error(("Collision of file names due case-insensitivity:" :: collisions).mkString("\n  "))
+    }
+  }
 }
 
 

--- a/src/Pure/Thy/sessions.scala	Tue Mar 12 15:34:33 2019 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Mar 13 13:46:16 2019 +0100
@@ -364,6 +364,10 @@
             val sources_errors =
               for (p <- session_files if !p.is_file) yield "No such file: " + p
 
+            val path_errors =
+              try { Path.check_case_insensitive(session_files ::: imported_files); Nil }
+              catch { case ERROR(msg) => List(msg) }
+
             val bibtex_errors =
               try { info.bibtex_entries; Nil }
               catch { case ERROR(msg) => List(msg) }
@@ -380,7 +384,7 @@
                 imported_sources = check_sources(imported_files),
                 sources = check_sources(session_files),
                 session_graph_display = session_graph_display,
-                errors = dependencies.errors ::: sources_errors ::: bibtex_errors,
+                errors = dependencies.errors ::: sources_errors ::: path_errors ::: bibtex_errors,
                 imports = Some(imports_base))
 
             session_bases + (info.name -> base)