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;
wenzelm@43651
     1
/*  Title:      Pure/Thy/thy_info.scala
wenzelm@43651
     2
    Author:     Makarius
wenzelm@43651
     3
wenzelm@43651
     4
Theory and file dependencies.
wenzelm@43651
     5
*/
wenzelm@43651
     6
wenzelm@43651
     7
package isabelle
wenzelm@43651
     8
wenzelm@43651
     9
wenzelm@43651
    10
class Thy_Info(thy_load: Thy_Load)
wenzelm@43651
    11
{
wenzelm@43651
    12
  /* messages */
wenzelm@43651
    13
wenzelm@44615
    14
  private def show_path(names: List[Document.Node.Name]): String =
wenzelm@44615
    15
    names.map(name => quote(name.theory)).mkString(" via ")
wenzelm@43651
    16
wenzelm@44615
    17
  private def cycle_msg(names: List[Document.Node.Name]): String =
wenzelm@43651
    18
    "Cyclic dependency of " + show_path(names)
wenzelm@43651
    19
wenzelm@44615
    20
  private def required_by(initiators: List[Document.Node.Name]): String =
wenzelm@43651
    21
    if (initiators.isEmpty) ""
wenzelm@44615
    22
    else "\n(required by " + show_path(initiators.reverse) + ")"
wenzelm@43651
    23
wenzelm@43651
    24
wenzelm@43651
    25
  /* dependencies */
wenzelm@43651
    26
wenzelm@48707
    27
  type Dep = (Document.Node.Name, Document.Node.Header)
wenzelm@48871
    28
  private sealed case class Required(
wenzelm@48871
    29
    deps: List[Dep] = Nil,
wenzelm@48871
    30
    seen: Set[Document.Node.Name] = Set.empty)
wenzelm@48871
    31
  {
wenzelm@48871
    32
    def :: (dep: Dep): Required = copy(deps = dep :: deps)
wenzelm@48871
    33
    def + (name: Document.Node.Name): Required = copy(seen = seen + name)
wenzelm@48871
    34
  }
wenzelm@43651
    35
wenzelm@44615
    36
  private def require_thys(initiators: List[Document.Node.Name],
wenzelm@44954
    37
      required: Required, names: List[Document.Node.Name]): Required =
wenzelm@44954
    38
    (required /: names)(require_thy(initiators, _, _))
wenzelm@44615
    39
wenzelm@44615
    40
  private def require_thy(initiators: List[Document.Node.Name],
wenzelm@44954
    41
      required: Required, name: Document.Node.Name): Required =
wenzelm@44615
    42
  {
wenzelm@48871
    43
    if (required.seen(name)) required
wenzelm@48871
    44
    else if (thy_load.loaded_theories(name.theory)) required + name
wenzelm@43651
    45
    else {
wenzelm@43651
    46
      try {
wenzelm@44615
    47
        if (initiators.contains(name)) error(cycle_msg(initiators))
wenzelm@48707
    48
        val header =
wenzelm@44615
    49
          try { thy_load.check_thy(name) }
wenzelm@43651
    50
          catch {
wenzelm@43651
    51
            case ERROR(msg) =>
wenzelm@44615
    52
              cat_error(msg, "The error(s) above occurred while examining theory " +
wenzelm@44615
    53
                quote(name.theory) + required_by(initiators))
wenzelm@43651
    54
          }
wenzelm@48871
    55
        (name, header) :: require_thys(name :: initiators, required + name, header.imports)
wenzelm@43651
    56
      }
wenzelm@48707
    57
      catch {
wenzelm@48707
    58
        case e: Throwable =>
wenzelm@48871
    59
          (name, Document.Node.bad_header(Exn.message(e))) :: (required + name)
wenzelm@48707
    60
      }
wenzelm@43651
    61
    }
wenzelm@43651
    62
  }
wenzelm@43651
    63
wenzelm@44954
    64
  def dependencies(names: List[Document.Node.Name]): List[Dep] =
wenzelm@48871
    65
    require_thys(Nil, Required(), names).deps.reverse
wenzelm@43651
    66
}