diff -r 9bfb6978eb80 -r 70898d016538 src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Tue Jul 24 20:42:34 2012 +0200
+++ b/src/Pure/Thy/thy_load.scala	Tue Jul 24 20:56:18 2012 +0200
@@ -13,6 +13,10 @@
 object Thy_Load
 {
   def thy_path(path: Path): Path = path.ext("thy")
+
+  def is_ok(str: String): Boolean =
+    try { thy_path(Path.explode(str)); true }
+    catch { case ERROR(_) => false }
 }