theory name needs to conform to Path syntax;
authorwenzelm
Tue Jul 05 22:38:44 2011 +0200 (2011-07-05)
changeset 43672e9f26e66692d
parent 43671 a250b092ac66
child 43673 29eb1cd29961
theory name needs to conform to Path syntax;
src/Pure/Thy/thy_header.scala
     1.1 --- a/src/Pure/Thy/thy_header.scala	Tue Jul 05 21:53:59 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Tue Jul 05 22:38:44 2011 +0200
     1.3 @@ -112,7 +112,8 @@
     1.4    {
     1.5      val header = read(source)
     1.6      val name1 = header.name
     1.7 -    if (name == name1) header
     1.8 -    else error("Bad file name " + thy_path(name) + " for theory " + quote(name1))
     1.9 +    if (name != name1) error("Bad file name " + thy_path(name) + " for theory " + quote(name1))
    1.10 +    Path.explode(name)
    1.11 +    header
    1.12    }
    1.13  }