# HG changeset patch # User wenzelm # Date 1512752249 -3600 # Node ID 39f57f0757f185b707181b175e8ba3d9da9e59aa # Parent 257bcd20eeecdb154d55fb14b06aa15810ba4984 clarified error; diff -r 257bcd20eeec -r 39f57f0757f1 src/Pure/Thy/thy_header.ML --- a/src/Pure/Thy/thy_header.ML Fri Dec 08 16:02:44 2017 +0100 +++ b/src/Pure/Thy/thy_header.ML Fri Dec 08 17:57:29 2017 +0100 @@ -118,7 +118,10 @@ fun is_base_name s = s <> "" andalso not (exists_string (member (op =) ["/", "\\", ":"]) s) -val import_name = Path.base_name o Path.explode; +fun import_name s = + if String.isSuffix ".thy" s then + error ("Malformed theory import: " ^ quote s) + else Path.base_name (Path.explode s); (* header args *) diff -r 257bcd20eeec -r 39f57f0757f1 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Fri Dec 08 16:02:44 2017 +0100 +++ b/src/Pure/Thy/thy_header.scala Fri Dec 08 17:57:29 2017 +0100 @@ -85,7 +85,10 @@ s != "" && !s.exists("/\\:".contains(_)) def import_name(s: String): String = - s match { case Import_Name(name) => name case _ => error("Malformed import: " + quote(s)) } + s match { + case Import_Name(name) if !name.endsWith(".thy") => name + case _ => error("Malformed theory import: " + quote(s)) + } def theory_name(s: String): String = s match {