src/Pure/Thy/thy_info.scala
author wenzelm
Fri Sep 29 20:49:42 2017 +0200 (2017-09-29)
changeset 66717 67dbf5cdc056
parent 66715 6bced18e2b91
child 66719 d37efafd55b5
permissions -rw-r--r--
more informative loaded_theories: dependencies and syntax;
     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, Nil, Nil, Set.empty)
    30   }
    31 
    32   final class Dependencies private(
    33     rev_entries: List[Document.Node.Entry],
    34     val keywords: Thy_Header.Keywords,
    35     val abbrevs: Thy_Header.Abbrevs,
    36     val seen: Set[Document.Node.Name])
    37   {
    38     def :: (entry: Document.Node.Entry): Dependencies =
    39       new Dependencies(
    40         entry :: rev_entries,
    41         entry.header.keywords ::: keywords,
    42         entry.header.abbrevs ::: abbrevs,
    43         seen)
    44 
    45     def + (name: Document.Node.Name): Dependencies =
    46       new Dependencies(rev_entries, keywords, abbrevs, seen + name)
    47 
    48     def entries: List[Document.Node.Entry] = rev_entries.reverse
    49     def names: List[Document.Node.Name] = entries.map(_.name)
    50 
    51     def errors: List[String] = entries.flatMap(_.header.errors)
    52 
    53     lazy val syntax: Outer_Syntax =
    54       resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
    55 
    56     def loaded_theories: Graph[String, Outer_Syntax] =
    57       (resources.session_base.loaded_theories /: entries)({ case (graph, entry) =>
    58         val name = entry.name.theory
    59         val imports = entry.header.imports.map(p => p._1.theory)
    60 
    61         if (graph.defined(name))
    62           error("Duplicate loaded theory entry " + quote(name))
    63 
    64         for (dep <- imports if !graph.defined(dep))
    65           error("Missing loaded theory entry " + quote(dep) + " for " + quote(name))
    66 
    67         val syntax = Outer_Syntax.merge(imports.map(graph.get_node(_))) + entry.header
    68         (graph.new_node(name, syntax) /: imports)((g, dep) => g.add_edge(dep, name))
    69       })
    70 
    71     def loaded_files: List[(String, List[Path])] =
    72     {
    73       names.map(_.theory) zip
    74         Par_List.map((e: () => List[Path]) => e(), names.map(resources.loaded_files(syntax, _)))
    75     }
    76 
    77     override def toString: String = entries.toString
    78   }
    79 
    80   private def require_thys(initiators: List[Document.Node.Name], required: Dependencies,
    81       thys: List[(Document.Node.Name, Position.T)]): Dependencies =
    82     (required /: thys)(require_thy(initiators, _, _))
    83 
    84   private def require_thy(initiators: List[Document.Node.Name], required: Dependencies,
    85     thy: (Document.Node.Name, Position.T)): Dependencies =
    86   {
    87     val (name, pos) = thy
    88 
    89     def message: String =
    90       "The error(s) above occurred for theory " + quote(name.theory) +
    91         required_by(initiators) + Position.here(pos)
    92 
    93     val required1 = required + name
    94     if (required.seen(name)) required
    95     else if (resources.session_base.loaded_theory(name)) required1
    96     else {
    97       try {
    98         if (initiators.contains(name)) error(cycle_msg(initiators))
    99         val header =
   100           try { resources.check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
   101           catch { case ERROR(msg) => cat_error(msg, message) }
   102         Document.Node.Entry(name, header) ::
   103           require_thys(name :: initiators, required1, header.imports)
   104       }
   105       catch {
   106         case e: Throwable =>
   107           Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1
   108       }
   109     }
   110   }
   111 
   112   def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies =
   113     require_thys(Nil, Dependencies.empty, thys)
   114 }