src/Pure/Thy/thy_info.scala
changeset 43674 3ddaa75c669c
parent 43673 29eb1cd29961
child 44159 9a35e88d9dc9
equal deleted inserted replaced
43673:29eb1cd29961 43674:3ddaa75c669c
    68       catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
    68       catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
    69     }
    69     }
    70   }
    70   }
    71 
    71 
    72   def dependencies(dir: Path, str: String): Deps =
    72   def dependencies(dir: Path, str: String): Deps =
    73     require_thy(thy_load.is_loaded, Nil, dir, Map.empty, str)  // FIXME capture errors in str (!??)
    73     require_thy(thy_load.is_loaded, Nil, dir, Map.empty, str)
    74 }
    74 }