src/Pure/Thy/thy_info.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 63584 68751fe1c036
child 65355 403eabd73c9a
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Pure/Thy/thy_info.scala
     2     Author:     Makarius
     3 
     4 Theory and file dependencies.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Thy_Info
    11 {
    12   /* dependencies */
    13 
    14   sealed case class Dep(
    15     name: Document.Node.Name,
    16     header: Document.Node.Header)
    17   {
    18     override def toString: String = name.toString
    19   }
    20 }
    21 
    22 class Thy_Info(resources: Resources)
    23 {
    24   /* messages */
    25 
    26   private def show_path(names: List[Document.Node.Name]): String =
    27     names.map(name => quote(name.theory)).mkString(" via ")
    28 
    29   private def cycle_msg(names: List[Document.Node.Name]): String =
    30     "Cyclic dependency of " + show_path(names)
    31 
    32   private def required_by(initiators: List[Document.Node.Name]): String =
    33     if (initiators.isEmpty) ""
    34     else "\n(required by " + show_path(initiators.reverse) + ")"
    35 
    36 
    37   /* dependencies */
    38 
    39   object Dependencies
    40   {
    41     val empty = new Dependencies(Nil, Nil, Nil, Set.empty, Multi_Map.empty, Multi_Map.empty)
    42   }
    43 
    44   final class Dependencies private(
    45     rev_deps: List[Thy_Info.Dep],
    46     val keywords: Thy_Header.Keywords,
    47     val abbrevs: Thy_Header.Abbrevs,
    48     val seen: Set[Document.Node.Name],
    49     val seen_names: Multi_Map[String, Document.Node.Name],
    50     val seen_positions: Multi_Map[String, Position.T])
    51   {
    52     def :: (dep: Thy_Info.Dep): Dependencies =
    53       new Dependencies(
    54         dep :: rev_deps, dep.header.keywords ::: keywords, dep.header.abbrevs ::: abbrevs,
    55         seen, seen_names, seen_positions)
    56 
    57     def + (thy: (Document.Node.Name, Position.T)): Dependencies =
    58     {
    59       val (name, pos) = thy
    60       new Dependencies(rev_deps, keywords, abbrevs,
    61         seen + name,
    62         seen_names + (name.theory -> name),
    63         seen_positions + (name.theory -> pos))
    64     }
    65 
    66     def deps: List[Thy_Info.Dep] = rev_deps.reverse
    67 
    68     def errors: List[String] =
    69     {
    70       val header_errors = deps.flatMap(dep => dep.header.errors)
    71       val import_errors =
    72         (for {
    73           (theory, names) <- seen_names.iterator_list
    74           if !resources.base.loaded_theories(theory)
    75           if names.length > 1
    76         } yield
    77           "Incoherent imports for theory " + quote(theory) + ":\n" +
    78             cat_lines(names.flatMap(name =>
    79               seen_positions.get_list(theory).map(pos =>
    80                 "  " + quote(name.node) + Position.here(pos))))
    81         ).toList
    82       header_errors ::: import_errors
    83     }
    84 
    85     lazy val syntax: Outer_Syntax =
    86       resources.base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
    87 
    88     def loaded_theories: Set[String] =
    89       (resources.base.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
    90 
    91     def loaded_files: List[Path] =
    92     {
    93       def loaded(dep: Thy_Info.Dep): List[Path] =
    94       {
    95         val string = resources.with_thy_reader(dep.name,
    96           reader => Symbol.decode(reader.source.toString))
    97         resources.loaded_files(syntax, string).
    98           map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
    99       }
   100       val dep_files = Par_List.map(loaded _, rev_deps)
   101       ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files }
   102     }
   103 
   104     override def toString: String = deps.toString
   105   }
   106 
   107   private def require_thys(session: String, initiators: List[Document.Node.Name],
   108       required: Dependencies, thys: List[(Document.Node.Name, Position.T)]): Dependencies =
   109     (required /: thys)(require_thy(session, initiators, _, _))
   110 
   111   private def require_thy(session: String, initiators: List[Document.Node.Name],
   112       required: Dependencies, thy: (Document.Node.Name, Position.T)): Dependencies =
   113   {
   114     val (name, require_pos) = thy
   115 
   116     def message: String =
   117       "The error(s) above occurred for theory " + quote(name.theory) +
   118         required_by(initiators) + Position.here(require_pos)
   119 
   120     val required1 = required + thy
   121     if (required.seen(name) || resources.base.loaded_theories(name.theory)) required1
   122     else {
   123       try {
   124         if (initiators.contains(name)) error(cycle_msg(initiators))
   125         val header =
   126           try { resources.check_thy(session, name, Token.Pos.file(name.node)).cat_errors(message) }
   127           catch { case ERROR(msg) => cat_error(msg, message) }
   128         Thy_Info.Dep(name, header) ::
   129           require_thys(session, name :: initiators, required1, header.imports)
   130       }
   131       catch {
   132         case e: Throwable =>
   133           Thy_Info.Dep(name, Document.Node.bad_header(Exn.message(e))) :: required1
   134       }
   135     }
   136   }
   137 
   138   def dependencies(session: String, thys: List[(Document.Node.Name, Position.T)]): Dependencies =
   139     require_thys(session, Nil, Dependencies.empty, thys)
   140 }