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