src/Pure/Thy/thy_info.scala
author wenzelm
Wed Apr 12 22:32:55 2017 +0200 (2017-04-12 ago)
changeset 65471 05e5bffcf1d8
parent 65439 862bfd2b4fd4
child 65507 decdb95bd007
permissions -rw-r--r--
clarified loaded_theories: map to qualified theory name;
proper theory_name for PIDE editors;
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@60077
    10
object Thy_Info
wenzelm@60077
    11
{
wenzelm@60077
    12
  /* dependencies */
wenzelm@60077
    13
wenzelm@60077
    14
  sealed case class Dep(
wenzelm@60077
    15
    name: Document.Node.Name,
wenzelm@60077
    16
    header: Document.Node.Header)
wenzelm@62865
    17
  {
wenzelm@62865
    18
    override def toString: String = name.toString
wenzelm@62865
    19
  }
wenzelm@60077
    20
}
wenzelm@60077
    21
wenzelm@56208
    22
class Thy_Info(resources: Resources)
wenzelm@43651
    23
{
wenzelm@43651
    24
  /* messages */
wenzelm@43651
    25
wenzelm@44615
    26
  private def show_path(names: List[Document.Node.Name]): String =
wenzelm@44615
    27
    names.map(name => quote(name.theory)).mkString(" via ")
wenzelm@43651
    28
wenzelm@44615
    29
  private def cycle_msg(names: List[Document.Node.Name]): String =
wenzelm@43651
    30
    "Cyclic dependency of " + show_path(names)
wenzelm@43651
    31
wenzelm@44615
    32
  private def required_by(initiators: List[Document.Node.Name]): String =
wenzelm@43651
    33
    if (initiators.isEmpty) ""
wenzelm@44615
    34
    else "\n(required by " + show_path(initiators.reverse) + ")"
wenzelm@43651
    35
wenzelm@43651
    36
wenzelm@43651
    37
  /* dependencies */
wenzelm@43651
    38
wenzelm@48872
    39
  object Dependencies
wenzelm@48872
    40
  {
wenzelm@65404
    41
    val empty = new Dependencies(Nil, Nil, Nil, Set.empty, Multi_Map.empty)
wenzelm@48872
    42
  }
wenzelm@48872
    43
wenzelm@48872
    44
  final class Dependencies private(
wenzelm@60077
    45
    rev_deps: List[Thy_Info.Dep],
wenzelm@48873
    46
    val keywords: Thy_Header.Keywords,
wenzelm@63579
    47
    val abbrevs: Thy_Header.Abbrevs,
wenzelm@61537
    48
    val seen: Set[Document.Node.Name],
wenzelm@65404
    49
    val seen_theory: Multi_Map[String, (Document.Node.Name, Position.T)])
wenzelm@48871
    50
  {
wenzelm@60077
    51
    def :: (dep: Thy_Info.Dep): Dependencies =
wenzelm@63579
    52
      new Dependencies(
wenzelm@63579
    53
        dep :: rev_deps, dep.header.keywords ::: keywords, dep.header.abbrevs ::: abbrevs,
wenzelm@65404
    54
        seen, seen_theory)
wenzelm@48873
    55
wenzelm@55488
    56
    def + (thy: (Document.Node.Name, Position.T)): Dependencies =
wenzelm@55488
    57
    {
wenzelm@65404
    58
      val (name, _) = thy
wenzelm@65406
    59
      new Dependencies(rev_deps, keywords, abbrevs, seen + name, seen_theory + (name.theory -> thy))
wenzelm@55488
    60
    }
wenzelm@48872
    61
wenzelm@60077
    62
    def deps: List[Thy_Info.Dep] = rev_deps.reverse
wenzelm@48872
    63
wenzelm@55488
    64
    def errors: List[String] =
wenzelm@55488
    65
    {
wenzelm@55488
    66
      val header_errors = deps.flatMap(dep => dep.header.errors)
wenzelm@55488
    67
      val import_errors =
wenzelm@55488
    68
        (for {
wenzelm@65404
    69
          (theory, imports) <- seen_theory.iterator_list
wenzelm@65429
    70
          if !resources.session_base.loaded_theories.isDefinedAt(theory)
wenzelm@65404
    71
          if imports.length > 1
wenzelm@65404
    72
        } yield {
wenzelm@55488
    73
          "Incoherent imports for theory " + quote(theory) + ":\n" +
wenzelm@65404
    74
            cat_lines(imports.map({ case (name, pos) =>
wenzelm@65404
    75
              "  " + quote(name.node) + Position.here(pos) }))
wenzelm@65404
    76
        }).toList
wenzelm@55488
    77
      header_errors ::: import_errors
wenzelm@55488
    78
    }
wenzelm@54549
    79
wenzelm@63584
    80
    lazy val syntax: Outer_Syntax =
wenzelm@65361
    81
      resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
wenzelm@51294
    82
wenzelm@65471
    83
    def loaded_theories: Map[String, String] =
wenzelm@65361
    84
      (resources.session_base.loaded_theories /: rev_deps) {
wenzelm@65408
    85
        case (loaded, dep) =>
wenzelm@65471
    86
          val name = dep.name
wenzelm@65471
    87
          loaded + (name.theory -> name.theory) +
wenzelm@65471
    88
            (name.theory_base_name -> name.theory)  // legacy
wenzelm@65361
    89
      }
wenzelm@48872
    90
wenzelm@56392
    91
    def loaded_files: List[Path] =
wenzelm@51294
    92
    {
wenzelm@60077
    93
      def loaded(dep: Thy_Info.Dep): List[Path] =
wenzelm@60077
    94
      {
wenzelm@60077
    95
        val string = resources.with_thy_reader(dep.name,
wenzelm@60077
    96
          reader => Symbol.decode(reader.source.toString))
wenzelm@60077
    97
        resources.loaded_files(syntax, string).
wenzelm@60077
    98
          map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
wenzelm@60077
    99
      }
wenzelm@60077
   100
      val dep_files = Par_List.map(loaded _, rev_deps)
wenzelm@59136
   101
      ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files }
wenzelm@51294
   102
    }
wenzelm@62865
   103
wenzelm@65405
   104
    def session_graph(parent_session: String, parent_base: Sessions.Base): Graph_Display.Graph =
wenzelm@65405
   105
    {
wenzelm@65405
   106
      val parent_session_node =
wenzelm@65405
   107
        Graph_Display.Node("[" + parent_session + "]", "session." + parent_session)
wenzelm@65405
   108
wenzelm@65405
   109
      def node(name: Document.Node.Name): Graph_Display.Node =
wenzelm@65405
   110
        if (parent_base.loaded_theory(name)) parent_session_node
wenzelm@65439
   111
        else Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
wenzelm@65405
   112
wenzelm@65405
   113
      (Graph_Display.empty_graph /: deps) {
wenzelm@65405
   114
        case (g, dep) =>
wenzelm@65405
   115
          if (parent_base.loaded_theory(dep.name)) g
wenzelm@65405
   116
          else {
wenzelm@65405
   117
            val a = node(dep.name)
wenzelm@65405
   118
            val bs = dep.header.imports.map({ case (name, _) => node(name) })
wenzelm@65405
   119
            ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a))
wenzelm@65405
   120
          }
wenzelm@65405
   121
      }
wenzelm@65405
   122
    }
wenzelm@65405
   123
wenzelm@62865
   124
    override def toString: String = deps.toString
wenzelm@48871
   125
  }
wenzelm@43651
   126
wenzelm@65359
   127
  private def require_thys(initiators: List[Document.Node.Name], required: Dependencies,
wenzelm@65359
   128
      thys: List[(Document.Node.Name, Position.T)]): Dependencies =
wenzelm@65359
   129
    (required /: thys)(require_thy(initiators, _, _))
wenzelm@44615
   130
wenzelm@65359
   131
  private def require_thy(initiators: List[Document.Node.Name], required: Dependencies,
wenzelm@65359
   132
    thy: (Document.Node.Name, Position.T)): Dependencies =
wenzelm@44615
   133
  {
wenzelm@55488
   134
    val (name, require_pos) = thy
wenzelm@55488
   135
wenzelm@55488
   136
    def message: String =
wenzelm@61537
   137
      "The error(s) above occurred for theory " + quote(name.theory) +
wenzelm@55488
   138
        required_by(initiators) + Position.here(require_pos)
wenzelm@55488
   139
wenzelm@55488
   140
    val required1 = required + thy
wenzelm@65404
   141
    if (required.seen(name)) required
wenzelm@65404
   142
    else if (resources.session_base.loaded_theory(name)) required1
wenzelm@43651
   143
    else {
wenzelm@43651
   144
      try {
wenzelm@44615
   145
        if (initiators.contains(name)) error(cycle_msg(initiators))
wenzelm@51294
   146
        val header =
wenzelm@65359
   147
          try { resources.check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
wenzelm@54549
   148
          catch { case ERROR(msg) => cat_error(msg, message) }
wenzelm@65359
   149
        Thy_Info.Dep(name, header) :: require_thys(name :: initiators, required1, header.imports)
wenzelm@43651
   150
      }
wenzelm@48707
   151
      catch {
wenzelm@48707
   152
        case e: Throwable =>
wenzelm@60077
   153
          Thy_Info.Dep(name, Document.Node.bad_header(Exn.message(e))) :: required1
wenzelm@48707
   154
      }
wenzelm@43651
   155
    }
wenzelm@43651
   156
  }
wenzelm@43651
   157
wenzelm@65359
   158
  def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies =
wenzelm@65359
   159
    require_thys(Nil, Dependencies.empty, thys)
wenzelm@43651
   160
}