src/Pure/Thy/thy_header.scala
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)) }