src/Pure/Thy/thy_info.scala
author wenzelm
Tue Feb 11 17:44:29 2014 +0100 (2014-02-11)
changeset 55431 e0f20a44ff9d
parent 54722 5f5608bfe230
child 55488 60c159d490a2
permissions -rw-r--r--
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
more informative type Blob, to allow markup reports;
     1 /*  Title:      Pure/Thy/thy_info.scala
     2     Author:     Makarius
     3 
     4 Theory and file dependencies.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.util.concurrent.{Future => JFuture}
    11 
    12 
    13 class Thy_Info(thy_load: Thy_Load)
    14 {
    15   /* messages */
    16 
    17   private def show_path(names: List[Document.Node.Name]): String =
    18     names.map(name => quote(name.theory)).mkString(" via ")
    19 
    20   private def cycle_msg(names: List[Document.Node.Name]): String =
    21     "Cyclic dependency of " + show_path(names)
    22 
    23   private def required_by(initiators: List[Document.Node.Name]): String =
    24     if (initiators.isEmpty) ""
    25     else "\n(required by " + show_path(initiators.reverse) + ")"
    26 
    27 
    28   /* dependencies */
    29 
    30   sealed case class Dep(
    31     name: Document.Node.Name,
    32     header: Document.Node.Header)
    33   {
    34     def load_files(syntax: Outer_Syntax): List[String] =
    35     {
    36       val string = thy_load.with_thy_text(name, _.toString)
    37       if (thy_load.body_files_test(syntax, string))
    38         thy_load.body_files(syntax, string)
    39       else Nil
    40     }
    41   }
    42 
    43   object Dependencies
    44   {
    45     val empty = new Dependencies(Nil, Nil, Set.empty)
    46   }
    47 
    48   final class Dependencies private(
    49     rev_deps: List[Dep],
    50     val keywords: Thy_Header.Keywords,
    51     val seen: Set[Document.Node.Name])
    52   {
    53     def :: (dep: Dep): Dependencies =
    54       new Dependencies(dep :: rev_deps, dep.header.keywords ::: keywords, seen)
    55 
    56     def + (name: Document.Node.Name): Dependencies =
    57       new Dependencies(rev_deps, keywords, seen = seen + name)
    58 
    59     def deps: List[Dep] = rev_deps.reverse
    60 
    61     def errors: List[String] = deps.flatMap(dep => dep.header.errors)
    62 
    63     lazy val syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
    64 
    65     def loaded_theories: Set[String] =
    66       (thy_load.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
    67 
    68     def load_files: List[Path] =
    69     {
    70       val dep_files =
    71         rev_deps.par.map(dep =>
    72           Exn.capture {
    73             dep.load_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
    74           }).toList
    75       ((Nil: List[Path]) /: dep_files) {
    76         case (acc_files, files) => Exn.release(files) ::: acc_files
    77       }
    78     }
    79   }
    80 
    81   private def require_thys(initiators: List[Document.Node.Name],
    82       required: Dependencies, names: List[Document.Node.Name]): Dependencies =
    83     (required /: names)(require_thy(initiators, _, _))
    84 
    85   private def require_thy(initiators: List[Document.Node.Name],
    86       required: Dependencies, name: Document.Node.Name): Dependencies =
    87   {
    88     if (required.seen(name)) required
    89     else if (thy_load.loaded_theories(name.theory)) required + name
    90     else {
    91       def message: String =
    92         "The error(s) above occurred for theory " + quote(name.theory) + required_by(initiators)
    93 
    94       try {
    95         if (initiators.contains(name)) error(cycle_msg(initiators))
    96         val header =
    97           try { thy_load.check_thy(name).cat_errors(message) }
    98           catch { case ERROR(msg) => cat_error(msg, message) }
    99         Dep(name, header) :: require_thys(name :: initiators, required + name, header.imports)
   100       }
   101       catch {
   102         case e: Throwable =>
   103           Dep(name, Document.Node.bad_header(Exn.message(e))) :: (required + name)
   104       }
   105     }
   106   }
   107 
   108   def dependencies(names: List[Document.Node.Name]): Dependencies =
   109     require_thys(Nil, Dependencies.empty, names)
   110 }