changeset 65526 | 41dda3a292e6 |
parent 65490 | 571a3ce3cc17 |
child 65539 | dbcd9b3e1b49 |
--- a/src/Pure/Thy/thy_header.scala Thu Apr 20 17:34:31 2017 +0200 +++ b/src/Pure/Thy/thy_header.scala Thu Apr 20 17:45:42 2017 +0200 @@ -81,6 +81,9 @@ private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""") private val Import_Name = new Regex(""".*?([^/\\:]+)""") + def is_base_name(s: String): Boolean = + s != "" && !s.exists("/\\:".contains(_)) + def import_name(s: String): String = s match { case Import_Name(name) => name case _ => error("Malformed import: " + quote(s)) }