src/Pure/Thy/thy_info.scala
author wenzelm
Sat Oct 07 13:13:46 2017 +0200 (19 months ago)
changeset 66776 b74b9d0bf763
parent 66775 e8f27a35ee0f
permissions -rw-r--r--
clarified empty merge;
tuned;
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@66719
    29
    val empty = new Dependencies(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@66711
    34
    val seen: Set[Document.Node.Name])
wenzelm@48871
    35
  {
wenzelm@66714
    36
    def :: (entry: Document.Node.Entry): Dependencies =
wenzelm@66719
    37
      new Dependencies(entry :: rev_entries, seen)
wenzelm@48873
    38
wenzelm@66711
    39
    def + (name: Document.Node.Name): Dependencies =
wenzelm@66719
    40
      new Dependencies(rev_entries, seen + name)
wenzelm@48872
    41
wenzelm@66714
    42
    def entries: List[Document.Node.Entry] = rev_entries.reverse
wenzelm@66715
    43
    def names: List[Document.Node.Name] = entries.map(_.name)
wenzelm@48872
    44
wenzelm@66714
    45
    def errors: List[String] = entries.flatMap(_.header.errors)
wenzelm@54549
    46
wenzelm@66719
    47
    lazy val loaded_theories: Graph[String, Outer_Syntax] =
wenzelm@66717
    48
      (resources.session_base.loaded_theories /: entries)({ case (graph, entry) =>
wenzelm@66717
    49
        val name = entry.name.theory
wenzelm@66717
    50
        val imports = entry.header.imports.map(p => p._1.theory)
wenzelm@66717
    51
wenzelm@66776
    52
        val graph1 = (graph /: (name :: imports))(_.default_node(_, Outer_Syntax.empty))
wenzelm@66775
    53
        val graph2 = (graph1 /: imports)(_.add_edge(_, name))
wenzelm@66717
    54
wenzelm@66776
    55
        val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil
wenzelm@66776
    56
        val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node(_))
wenzelm@66776
    57
        val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header
wenzelm@66776
    58
wenzelm@66775
    59
        graph2.map_node(name, _ => syntax)
wenzelm@66717
    60
      })
wenzelm@48872
    61
wenzelm@66701
    62
    def loaded_files: List[(String, List[Path])] =
wenzelm@51294
    63
    {
wenzelm@66701
    64
      names.map(_.theory) zip
wenzelm@66719
    65
        Par_List.map((e: () => List[Path]) => e(),
wenzelm@66719
    66
          names.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
wenzelm@51294
    67
    }
wenzelm@62865
    68
wenzelm@66743
    69
    def imported_files: List[Path] =
wenzelm@66743
    70
    {
wenzelm@66743
    71
      val base = resources.session_base
wenzelm@66743
    72
      val base_theories =
wenzelm@66743
    73
        loaded_theories.all_preds(names.map(_.theory)).
wenzelm@66743
    74
          filter(base.loaded_theories.defined(_))
wenzelm@66743
    75
wenzelm@66743
    76
      base_theories.map(theory => base.known.theories(theory).path) :::
wenzelm@66743
    77
      base_theories.flatMap(base.known.loaded_files(_))
wenzelm@66743
    78
    }
wenzelm@66743
    79
wenzelm@66719
    80
    lazy val overall_syntax: Outer_Syntax =
wenzelm@66719
    81
      Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node(_)))
wenzelm@66719
    82
wenzelm@66714
    83
    override def toString: String = entries.toString
wenzelm@48871
    84
  }
wenzelm@43651
    85
wenzelm@65359
    86
  private def require_thys(initiators: List[Document.Node.Name], required: Dependencies,
wenzelm@65359
    87
      thys: List[(Document.Node.Name, Position.T)]): Dependencies =
wenzelm@65359
    88
    (required /: thys)(require_thy(initiators, _, _))
wenzelm@44615
    89
wenzelm@65359
    90
  private def require_thy(initiators: List[Document.Node.Name], required: Dependencies,
wenzelm@65359
    91
    thy: (Document.Node.Name, Position.T)): Dependencies =
wenzelm@44615
    92
  {
wenzelm@66711
    93
    val (name, pos) = thy
wenzelm@55488
    94
wenzelm@55488
    95
    def message: String =
wenzelm@61536
    96
      "The error(s) above occurred for theory " + quote(name.theory) +
wenzelm@66711
    97
        required_by(initiators) + Position.here(pos)
wenzelm@55488
    98
wenzelm@66711
    99
    val required1 = required + name
wenzelm@65403
   100
    if (required.seen(name)) required
wenzelm@65403
   101
    else if (resources.session_base.loaded_theory(name)) required1
wenzelm@43651
   102
    else {
wenzelm@43651
   103
      try {
wenzelm@44615
   104
        if (initiators.contains(name)) error(cycle_msg(initiators))
wenzelm@51294
   105
        val header =
wenzelm@65359
   106
          try { resources.check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
wenzelm@54549
   107
          catch { case ERROR(msg) => cat_error(msg, message) }
wenzelm@66714
   108
        Document.Node.Entry(name, header) ::
wenzelm@66714
   109
          require_thys(name :: initiators, required1, header.imports)
wenzelm@43651
   110
      }
wenzelm@48707
   111
      catch {
wenzelm@48707
   112
        case e: Throwable =>
wenzelm@66714
   113
          Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1
wenzelm@48707
   114
      }
wenzelm@43651
   115
    }
wenzelm@43651
   116
  }
wenzelm@43651
   117
wenzelm@65359
   118
  def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies =
wenzelm@65359
   119
    require_thys(Nil, Dependencies.empty, thys)
wenzelm@43651
   120
}