src/Pure/Thy/thy_info.scala
author wenzelm
Fri Apr 25 20:07:39 2014 +0200 (2014-04-25)
changeset 56728 6dc97c5aaf5e
parent 56393 22f533e6a049
child 56801 8dd9df88f647
permissions -rw-r--r--
unused;
     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   sealed case class Dep(
    28     name: Document.Node.Name,
    29     header: Document.Node.Header)
    30   {
    31     def loaded_files(syntax: Prover.Syntax): List[String] =
    32     {
    33       val string = resources.with_thy_text(name, _.toString)
    34       resources.loaded_files(syntax, string)
    35     }
    36   }
    37 
    38   object Dependencies
    39   {
    40     val empty = new Dependencies(Nil, Nil, Multi_Map.empty, Multi_Map.empty)
    41   }
    42 
    43   final class Dependencies private(
    44     rev_deps: List[Dep],
    45     val keywords: Thy_Header.Keywords,
    46     val seen_names: Multi_Map[String, Document.Node.Name],
    47     val seen_positions: Multi_Map[String, Position.T])
    48   {
    49     def :: (dep: Dep): Dependencies =
    50       new Dependencies(dep :: rev_deps, dep.header.keywords ::: keywords,
    51         seen_names, seen_positions)
    52 
    53     def + (thy: (Document.Node.Name, Position.T)): Dependencies =
    54     {
    55       val (name, pos) = thy
    56       new Dependencies(rev_deps, keywords,
    57         seen_names + (name.theory -> name),
    58         seen_positions + (name.theory -> pos))
    59     }
    60 
    61     def deps: List[Dep] = rev_deps.reverse
    62 
    63     def errors: List[String] =
    64     {
    65       val header_errors = deps.flatMap(dep => dep.header.errors)
    66       val import_errors =
    67         (for {
    68           (theory, names) <- seen_names.iterator_list
    69           if !resources.loaded_theories(theory)
    70           if names.length > 1
    71         } yield
    72           "Incoherent imports for theory " + quote(theory) + ":\n" +
    73             cat_lines(names.flatMap(name =>
    74               seen_positions.get_list(theory).map(pos =>
    75                 "  " + quote(name.node) + Position.here(pos))))
    76         ).toList
    77       header_errors ::: import_errors
    78     }
    79 
    80     lazy val syntax: Prover.Syntax = resources.base_syntax.add_keywords(keywords)
    81 
    82     def loaded_theories: Set[String] =
    83       (resources.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
    84 
    85     def loaded_files: List[Path] =
    86     {
    87       val dep_files =
    88         rev_deps.par.map(dep =>
    89           Exn.capture {
    90             dep.loaded_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
    91           }).toList
    92       ((Nil: List[Path]) /: dep_files) {
    93         case (acc_files, files) => Exn.release(files) ::: acc_files
    94       }
    95     }
    96   }
    97 
    98   private def require_thys(initiators: List[Document.Node.Name],
    99       required: Dependencies, thys: List[(Document.Node.Name, Position.T)]): Dependencies =
   100     (required /: thys)(require_thy(initiators, _, _))
   101 
   102   private def require_thy(initiators: List[Document.Node.Name],
   103       required: Dependencies, thy: (Document.Node.Name, Position.T)): Dependencies =
   104   {
   105     val (name, require_pos) = thy
   106     val theory = name.theory
   107 
   108     def message: String =
   109       "The error(s) above occurred for theory " + quote(theory) +
   110         required_by(initiators) + Position.here(require_pos)
   111 
   112     val required1 = required + thy
   113     if (required.seen_names.isDefinedAt(theory) || resources.loaded_theories(theory))
   114       required1
   115     else {
   116       try {
   117         if (initiators.contains(name)) error(cycle_msg(initiators))
   118         val header =
   119           try { resources.check_thy(name).cat_errors(message) }
   120           catch { case ERROR(msg) => cat_error(msg, message) }
   121         val imports = header.imports.map((_, Position.File(name.node)))
   122         Dep(name, header) :: require_thys(name :: initiators, required1, imports)
   123       }
   124       catch {
   125         case e: Throwable =>
   126           Dep(name, Document.Node.bad_header(Exn.message(e))) :: required1
   127       }
   128     }
   129   }
   130 
   131   def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies =
   132     require_thys(Nil, Dependencies.empty, thys)
   133 }