clarified error;
authorwenzelm
Fri Dec 08 17:57:29 2017 +0100 (17 months ago)
changeset 6716439f57f0757f1
parent 67163 257bcd20eeec
child 67165 22a5822f52f7
child 67172 97d199699a6b
clarified error;
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
     1.1 --- a/src/Pure/Thy/thy_header.ML	Fri Dec 08 16:02:44 2017 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.ML	Fri Dec 08 17:57:29 2017 +0100
     1.3 @@ -118,7 +118,10 @@
     1.4  fun is_base_name s =
     1.5    s <> "" andalso not (exists_string (member (op =) ["/", "\\", ":"]) s)
     1.6  
     1.7 -val import_name = Path.base_name o Path.explode;
     1.8 +fun import_name s =
     1.9 +  if String.isSuffix ".thy" s then
    1.10 +    error ("Malformed theory import: " ^ quote s)
    1.11 +  else Path.base_name (Path.explode s);
    1.12  
    1.13  
    1.14  (* header args *)
     2.1 --- a/src/Pure/Thy/thy_header.scala	Fri Dec 08 16:02:44 2017 +0100
     2.2 +++ b/src/Pure/Thy/thy_header.scala	Fri Dec 08 17:57:29 2017 +0100
     2.3 @@ -85,7 +85,10 @@
     2.4      s != "" && !s.exists("/\\:".contains(_))
     2.5  
     2.6    def import_name(s: String): String =
     2.7 -    s match { case Import_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
     2.8 +    s match {
     2.9 +      case Import_Name(name) if !name.endsWith(".thy") => name
    2.10 +      case _ => error("Malformed theory import: " + quote(s))
    2.11 +    }
    2.12  
    2.13    def theory_name(s: String): String =
    2.14      s match {