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 } }