src/Pure/Thy/thy_info.scala
author wenzelm
Tue Aug 21 13:29:34 2012 +0200 (2012-08-21)
changeset 48871 c82720f054c3
parent 48870 4accee106f0f
child 48872 6124e0d1120a
permissions -rw-r--r--
tuned signature;
     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[Document.Node.Name]): String =
    15     names.map(name => quote(name.theory)).mkString(" via ")
    16 
    17   private def cycle_msg(names: List[Document.Node.Name]): String =
    18     "Cyclic dependency of " + show_path(names)
    19 
    20   private def required_by(initiators: List[Document.Node.Name]): String =
    21     if (initiators.isEmpty) ""
    22     else "\n(required by " + show_path(initiators.reverse) + ")"
    23 
    24 
    25   /* dependencies */
    26 
    27   type Dep = (Document.Node.Name, Document.Node.Header)
    28   private sealed case class Required(
    29     deps: List[Dep] = Nil,
    30     seen: Set[Document.Node.Name] = Set.empty)
    31   {
    32     def :: (dep: Dep): Required = copy(deps = dep :: deps)
    33     def + (name: Document.Node.Name): Required = copy(seen = seen + name)
    34   }
    35 
    36   private def require_thys(initiators: List[Document.Node.Name],
    37       required: Required, names: List[Document.Node.Name]): Required =
    38     (required /: names)(require_thy(initiators, _, _))
    39 
    40   private def require_thy(initiators: List[Document.Node.Name],
    41       required: Required, name: Document.Node.Name): Required =
    42   {
    43     if (required.seen(name)) required
    44     else if (thy_load.loaded_theories(name.theory)) required + name
    45     else {
    46       try {
    47         if (initiators.contains(name)) error(cycle_msg(initiators))
    48         val header =
    49           try { thy_load.check_thy(name) }
    50           catch {
    51             case ERROR(msg) =>
    52               cat_error(msg, "The error(s) above occurred while examining theory " +
    53                 quote(name.theory) + required_by(initiators))
    54           }
    55         (name, header) :: require_thys(name :: initiators, required + name, header.imports)
    56       }
    57       catch {
    58         case e: Throwable =>
    59           (name, Document.Node.bad_header(Exn.message(e))) :: (required + name)
    60       }
    61     }
    62   }
    63 
    64   def dependencies(names: List[Document.Node.Name]): List[Dep] =
    65     require_thys(Nil, Required(), names).deps.reverse
    66 }