src/Pure/Thy/thy_info.scala
author wenzelm
Sun Oct 01 17:59:26 2017 +0200 (21 months ago)
changeset 66743 ff05d922bc34
parent 66719 d37efafd55b5
child 66775 e8f27a35ee0f
permissions -rw-r--r--
cache sources: invoke SHA1.digest at most once;
maintain imported_sources, as required for new theories;
     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(resources: Resources)
    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   object Dependencies
    28   {
    29     val empty = new Dependencies(Nil, Set.empty)
    30   }
    31 
    32   final class Dependencies private(
    33     rev_entries: List[Document.Node.Entry],
    34     val seen: Set[Document.Node.Name])
    35   {
    36     def :: (entry: Document.Node.Entry): Dependencies =
    37       new Dependencies(entry :: rev_entries, seen)
    38 
    39     def + (name: Document.Node.Name): Dependencies =
    40       new Dependencies(rev_entries, seen + name)
    41 
    42     def entries: List[Document.Node.Entry] = rev_entries.reverse
    43     def names: List[Document.Node.Name] = entries.map(_.name)
    44 
    45     def errors: List[String] = entries.flatMap(_.header.errors)
    46 
    47     lazy val loaded_theories: Graph[String, Outer_Syntax] =
    48       (resources.session_base.loaded_theories /: entries)({ case (graph, entry) =>
    49         val name = entry.name.theory
    50         val imports = entry.header.imports.map(p => p._1.theory)
    51 
    52         if (graph.defined(name))
    53           error("Duplicate loaded theory entry " + quote(name))
    54 
    55         for (dep <- imports if !graph.defined(dep))
    56           error("Missing loaded theory entry " + quote(dep) + " for " + quote(name))
    57 
    58         val syntax = Outer_Syntax.merge(imports.map(graph.get_node(_))) + entry.header
    59         (graph.new_node(name, syntax) /: imports)((g, dep) => g.add_edge(dep, name))
    60       })
    61 
    62     def loaded_files: List[(String, List[Path])] =
    63     {
    64       names.map(_.theory) zip
    65         Par_List.map((e: () => List[Path]) => e(),
    66           names.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
    67     }
    68 
    69     def imported_files: List[Path] =
    70     {
    71       val base = resources.session_base
    72       val base_theories =
    73         loaded_theories.all_preds(names.map(_.theory)).
    74           filter(base.loaded_theories.defined(_))
    75 
    76       base_theories.map(theory => base.known.theories(theory).path) :::
    77       base_theories.flatMap(base.known.loaded_files(_))
    78     }
    79 
    80     lazy val overall_syntax: Outer_Syntax =
    81       Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node(_)))
    82 
    83     override def toString: String = entries.toString
    84   }
    85 
    86   private def require_thys(initiators: List[Document.Node.Name], required: Dependencies,
    87       thys: List[(Document.Node.Name, Position.T)]): Dependencies =
    88     (required /: thys)(require_thy(initiators, _, _))
    89 
    90   private def require_thy(initiators: List[Document.Node.Name], required: Dependencies,
    91     thy: (Document.Node.Name, Position.T)): Dependencies =
    92   {
    93     val (name, pos) = thy
    94 
    95     def message: String =
    96       "The error(s) above occurred for theory " + quote(name.theory) +
    97         required_by(initiators) + Position.here(pos)
    98 
    99     val required1 = required + name
   100     if (required.seen(name)) required
   101     else if (resources.session_base.loaded_theory(name)) required1
   102     else {
   103       try {
   104         if (initiators.contains(name)) error(cycle_msg(initiators))
   105         val header =
   106           try { resources.check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
   107           catch { case ERROR(msg) => cat_error(msg, message) }
   108         Document.Node.Entry(name, header) ::
   109           require_thys(name :: initiators, required1, header.imports)
   110       }
   111       catch {
   112         case e: Throwable =>
   113           Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1
   114       }
   115     }
   116   }
   117 
   118   def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies =
   119     require_thys(Nil, Dependencies.empty, thys)
   120 }