src/Pure/Thy/thy_info.scala
changeset 43673 29eb1cd29961
parent 43652 dcd0b667f73d
child 43674 3ddaa75c669c
equal deleted inserted replaced
43672:e9f26e66692d 43673:29eb1cd29961
     3 
     3 
     4 Theory and file dependencies.
     4 Theory and file dependencies.
     5 */
     5 */
     6 
     6 
     7 package isabelle
     7 package isabelle
       
     8 
       
     9 
       
    10 object Thy_Info
       
    11 {
       
    12   /* protocol messages */
       
    13 
       
    14   object Loaded_Theory {
       
    15     def unapply(msg: XML.Tree): Option[String] =
       
    16       msg match {
       
    17         case XML.Elem(Markup(Markup.LOADED_THEORY, List((Markup.NAME, name))), _) => Some(name)
       
    18         case _ => None
       
    19       }
       
    20   }
       
    21 }
     8 
    22 
     9 
    23 
    10 class Thy_Info(thy_load: Thy_Load)
    24 class Thy_Info(thy_load: Thy_Load)
    11 {
    25 {
    12   /* messages */
    26   /* messages */
    24 
    38 
    25   /* dependencies */
    39   /* dependencies */
    26 
    40 
    27   type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]]  // name -> (text, header)
    41   type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]]  // name -> (text, header)
    28 
    42 
    29   private def require_thys(
    43   private def require_thys(ignored: String => Boolean,
    30       initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
    44       initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
    31     (deps /: strs)(require_thy(initiators, dir, _, _))
    45     (deps /: strs)(require_thy(ignored, initiators, dir, _, _))
    32 
    46 
    33   private def require_thy(initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
    47   private def require_thy(ignored: String => Boolean,
       
    48       initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
    34   {
    49   {
    35     val path = Path.explode(str)
    50     val path = Path.explode(str)
    36     val name = path.base.implode
    51     val name = path.base.implode
    37 
    52 
    38     if (deps.isDefinedAt(name)) deps
    53     if (deps.isDefinedAt(name) || ignored(name)) deps
    39     else {
    54     else {
    40       val dir1 = dir + path.dir
    55       val dir1 = dir + path.dir
    41       try {
    56       try {
    42         if (initiators.contains(name)) error(cycle_msg(initiators))
    57         if (initiators.contains(name)) error(cycle_msg(initiators))
    43         val (text, header) =
    58         val (text, header) =
    45           catch {
    60           catch {
    46             case ERROR(msg) =>
    61             case ERROR(msg) =>
    47               cat_error(msg, "The error(s) above occurred while examining theory " +
    62               cat_error(msg, "The error(s) above occurred while examining theory " +
    48                 quote(name) + required_by("\n", initiators))
    63                 quote(name) + required_by("\n", initiators))
    49           }
    64           }
    50         require_thys(name :: initiators, dir1,
    65         require_thys(ignored, name :: initiators, dir1,
    51           deps + (name -> Exn.Res(text, header)), header.imports)
    66           deps + (name -> Exn.Res(text, header)), header.imports)
    52       }
    67       }
    53       catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
    68       catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
    54     }
    69     }
    55   }
    70   }
    56 
    71 
    57   def dependencies(dir: Path, str: String): Deps =
    72   def dependencies(dir: Path, str: String): Deps =
    58     require_thy(Nil, dir, Map.empty, str)  // FIXME capture errors in str (!??)
    73     require_thy(thy_load.is_loaded, Nil, dir, Map.empty, str)  // FIXME capture errors in str (!??)
    59 }
    74 }