changeset 48484 | 70898d016538 |
parent 48422 | 9613780a805b |
child 48707 | ba531af91148 |
--- 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 } }