# HG changeset patch # User wenzelm # Date 1552481176 -3600 # Node ID 6f5bd59f75f4f32d6cd2bcdc3d30dc9bd69c6b9c # Parent 63721ee8c86c528b5fe5f3dce27cd56efc2315a5 more sanity checks; diff -r 63721ee8c86c -r 6f5bd59f75f4 src/Pure/General/path.scala --- 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 ")) + } + } } diff -r 63721ee8c86c -r 6f5bd59f75f4 src/Pure/Thy/sessions.scala --- 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)