more errors;
authorwenzelm
Sat Jul 25 12:43:29 2020 +0200 (2 weeks ago)
changeset 72072fed7b0ae20d8
parent 72071 d3cad9ecd0cc
child 72073 f56522a44564
more errors;
src/Pure/PIDE/resources.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Fri Jul 24 20:43:32 2020 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Sat Jul 25 12:43:29 2020 +0200
     1.3 @@ -196,10 +196,15 @@
     1.4          val header = Thy_Header.read(reader, start, strict)
     1.5  
     1.6          val base_name = node_name.theory_base_name
     1.7 -        if (base_name != header.name)
     1.8 +        if (Long_Name.is_qualified(header.name)) {
     1.9 +          error("Bad theory name " + quote(header.name) + " with qualification" +
    1.10 +            Position.here(header.pos))
    1.11 +        }
    1.12 +        if (base_name != header.name) {
    1.13            error("Bad theory name " + quote(header.name) +
    1.14              " for file " + thy_path(Path.basic(base_name)) + Position.here(header.pos) +
    1.15              Completion.report_theories(header.pos, List(base_name)))
    1.16 +        }
    1.17  
    1.18          val imports_pos =
    1.19            header.imports_pos.map({ case (s, pos) =>