src/Pure/Thy/thy_load.scala
changeset 48484 70898d016538
parent 48422 9613780a805b
child 48707 ba531af91148
equal deleted inserted replaced
48483:9bfb6978eb80 48484:70898d016538
    11 
    11 
    12 
    12 
    13 object Thy_Load
    13 object Thy_Load
    14 {
    14 {
    15   def thy_path(path: Path): Path = path.ext("thy")
    15   def thy_path(path: Path): Path = path.ext("thy")
       
    16 
       
    17   def is_ok(str: String): Boolean =
       
    18     try { thy_path(Path.explode(str)); true }
       
    19     catch { case ERROR(_) => false }
    16 }
    20 }
    17 
    21 
    18 
    22 
    19 class Thy_Load(preloaded: Set[String] = Set.empty)
    23 class Thy_Load(preloaded: Set[String] = Set.empty)
    20 {
    24 {