more sanity checks;
authorwenzelm
Wed Mar 13 13:46:16 2019 +0100 (6 weeks ago ago)
changeset 700856f5bd59f75f4
parent 70084 63721ee8c86c
child 70086 06f204a2f3c2
more sanity checks;
src/Pure/General/path.scala
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/General/path.scala	Tue Mar 12 15:34:33 2019 +0100
     1.2 +++ b/src/Pure/General/path.scala	Wed Mar 13 13:46:16 2019 +0100
     1.3 @@ -130,6 +130,23 @@
     1.4  
     1.5    def is_reserved(name: String): Boolean =
     1.6      Long_Name.explode(name).exists(a => reserved_windows.contains(Word.uppercase(a)))
     1.7 +
     1.8 +
     1.9 +  /* case-insensitive names */
    1.10 +
    1.11 +  def check_case_insensitive(paths: List[Path])
    1.12 +  {
    1.13 +    val table =
    1.14 +      (Multi_Map.empty[String, String] /: paths)({ case (tab, path) =>
    1.15 +        val name = path.expand.implode
    1.16 +        tab.insert(Word.lowercase(name), name)
    1.17 +      })
    1.18 +    val collisions =
    1.19 +      (for { (_, coll) <- table.iterator_list if coll.length > 1 } yield coll).toList.flatten
    1.20 +    if (collisions.nonEmpty) {
    1.21 +      error(("Collision of file names due case-insensitivity:" :: collisions).mkString("\n  "))
    1.22 +    }
    1.23 +  }
    1.24  }
    1.25  
    1.26  
     2.1 --- a/src/Pure/Thy/sessions.scala	Tue Mar 12 15:34:33 2019 +0100
     2.2 +++ b/src/Pure/Thy/sessions.scala	Wed Mar 13 13:46:16 2019 +0100
     2.3 @@ -364,6 +364,10 @@
     2.4              val sources_errors =
     2.5                for (p <- session_files if !p.is_file) yield "No such file: " + p
     2.6  
     2.7 +            val path_errors =
     2.8 +              try { Path.check_case_insensitive(session_files ::: imported_files); Nil }
     2.9 +              catch { case ERROR(msg) => List(msg) }
    2.10 +
    2.11              val bibtex_errors =
    2.12                try { info.bibtex_entries; Nil }
    2.13                catch { case ERROR(msg) => List(msg) }
    2.14 @@ -380,7 +384,7 @@
    2.15                  imported_sources = check_sources(imported_files),
    2.16                  sources = check_sources(session_files),
    2.17                  session_graph_display = session_graph_display,
    2.18 -                errors = dependencies.errors ::: sources_errors ::: bibtex_errors,
    2.19 +                errors = dependencies.errors ::: sources_errors ::: path_errors ::: bibtex_errors,
    2.20                  imports = Some(imports_base))
    2.21  
    2.22              session_bases + (info.name -> base)