src/Pure/Thy/thy_info.scala
changeset 43651 511df47bcadc
child 43652 dcd0b667f73d
equal deleted inserted replaced
43650:f00da558b78e 43651:511df47bcadc
       
     1 /*  Title:      Pure/Thy/thy_info.scala
       
     2     Author:     Makarius
       
     3 
       
     4 Theory and file dependencies.
       
     5 */
       
     6 
       
     7 package isabelle
       
     8 
       
     9 
       
    10 class Thy_Info(thy_load: Thy_Load)
       
    11 {
       
    12   /* messages */
       
    13 
       
    14   private def show_path(names: List[String]): String =
       
    15     names.map(Library.quote).mkString(" via ")
       
    16 
       
    17   private def cycle_msg(names: List[String]): String =
       
    18     "Cyclic dependency of " + show_path(names)
       
    19 
       
    20   private def required_by(s: String, initiators: List[String]): String =
       
    21     if (initiators.isEmpty) ""
       
    22     else s + "(required by " + show_path(initiators.reverse) + ")"
       
    23 
       
    24 
       
    25   /* dependencies */
       
    26 
       
    27   type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]]  // name -> (text, header)
       
    28 
       
    29   private def require_thys(
       
    30       initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
       
    31     (deps /: strs)(require_thy(initiators, dir, _, _))
       
    32 
       
    33   private def require_thy(initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
       
    34   {
       
    35     val path = Path.explode(str)
       
    36     val name = path.base.implode
       
    37 
       
    38     if (deps.isDefinedAt(name)) deps
       
    39     else {
       
    40       val dir1 = dir + path.dir
       
    41       try {
       
    42         if (initiators.contains(name)) error(cycle_msg(initiators))
       
    43         val (text, header) =
       
    44           try { thy_load.check_thy(dir1, name) }
       
    45           catch {
       
    46             case ERROR(msg) =>
       
    47               cat_error(msg, "The error(s) above occurred while examining theory " +
       
    48                 Library.quote(name) + required_by("\n", initiators))
       
    49           }
       
    50         require_thys(name :: initiators, dir1,
       
    51           deps + (name -> Exn.Res(text, header)), header.imports)
       
    52       }
       
    53       catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
       
    54     }
       
    55   }
       
    56 
       
    57   def dependencies(dir: Path, str: String): Deps =
       
    58     require_thy(Nil, dir, Map.empty, str)  // FIXME capture errors in str (!??)
       
    59 }