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;
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@50414
    10
import java.util.concurrent.{Future => JFuture}
wenzelm@50414
    11
wenzelm@50414
    12
wenzelm@43651
    13
class Thy_Info(thy_load: Thy_Load)
wenzelm@43651
    14
{
wenzelm@43651
    15
  /* messages */
wenzelm@43651
    16
wenzelm@44615
    17
  private def show_path(names: List[Document.Node.Name]): String =
wenzelm@44615
    18
    names.map(name => quote(name.theory)).mkString(" via ")
wenzelm@43651
    19
wenzelm@44615
    20
  private def cycle_msg(names: List[Document.Node.Name]): String =
wenzelm@43651
    21
    "Cyclic dependency of " + show_path(names)
wenzelm@43651
    22
wenzelm@44615
    23
  private def required_by(initiators: List[Document.Node.Name]): String =
wenzelm@43651
    24
    if (initiators.isEmpty) ""
wenzelm@44615
    25
    else "\n(required by " + show_path(initiators.reverse) + ")"
wenzelm@43651
    26
wenzelm@43651
    27
wenzelm@43651
    28
  /* dependencies */
wenzelm@43651
    29
wenzelm@50414
    30
  sealed case class Dep(
wenzelm@50414
    31
    name: Document.Node.Name,
wenzelm@51294
    32
    header: Document.Node.Header)
wenzelm@50414
    33
  {
wenzelm@51294
    34
    def load_files(syntax: Outer_Syntax): List[String] =
wenzelm@51294
    35
    {
wenzelm@51294
    36
      val string = thy_load.with_thy_text(name, _.toString)
wenzelm@51294
    37
      if (thy_load.body_files_test(syntax, string))
wenzelm@51294
    38
        thy_load.body_files(syntax, string)
wenzelm@51294
    39
      else Nil
wenzelm@51294
    40
    }
wenzelm@50414
    41
  }
wenzelm@48872
    42
wenzelm@48872
    43
  object Dependencies
wenzelm@48872
    44
  {
wenzelm@48873
    45
    val empty = new Dependencies(Nil, Nil, Set.empty)
wenzelm@48872
    46
  }
wenzelm@48872
    47
wenzelm@48872
    48
  final class Dependencies private(
wenzelm@48872
    49
    rev_deps: List[Dep],
wenzelm@48873
    50
    val keywords: Thy_Header.Keywords,
wenzelm@48872
    51
    val seen: Set[Document.Node.Name])
wenzelm@48871
    52
  {
wenzelm@48873
    53
    def :: (dep: Dep): Dependencies =
wenzelm@51294
    54
      new Dependencies(dep :: rev_deps, dep.header.keywords ::: keywords, seen)
wenzelm@48873
    55
wenzelm@48873
    56
    def + (name: Document.Node.Name): Dependencies =
wenzelm@48873
    57
      new Dependencies(rev_deps, keywords, seen = seen + name)
wenzelm@48872
    58
wenzelm@48872
    59
    def deps: List[Dep] = rev_deps.reverse
wenzelm@48872
    60
wenzelm@54549
    61
    def errors: List[String] = deps.flatMap(dep => dep.header.errors)
wenzelm@54549
    62
wenzelm@51294
    63
    lazy val syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
wenzelm@51294
    64
wenzelm@48872
    65
    def loaded_theories: Set[String] =
wenzelm@50414
    66
      (thy_load.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
wenzelm@48872
    67
wenzelm@51294
    68
    def load_files: List[Path] =
wenzelm@51294
    69
    {
wenzelm@51298
    70
      val dep_files =
wenzelm@51298
    71
        rev_deps.par.map(dep =>
wenzelm@51298
    72
          Exn.capture {
wenzelm@54515
    73
            dep.load_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
wenzelm@51298
    74
          }).toList
wenzelm@51298
    75
      ((Nil: List[Path]) /: dep_files) {
wenzelm@51298
    76
        case (acc_files, files) => Exn.release(files) ::: acc_files
wenzelm@51294
    77
      }
wenzelm@51294
    78
    }
wenzelm@48871
    79
  }
wenzelm@43651
    80
wenzelm@51294
    81
  private def require_thys(initiators: List[Document.Node.Name],
wenzelm@48872
    82
      required: Dependencies, names: List[Document.Node.Name]): Dependencies =
wenzelm@51294
    83
    (required /: names)(require_thy(initiators, _, _))
wenzelm@44615
    84
wenzelm@51294
    85
  private def require_thy(initiators: List[Document.Node.Name],
wenzelm@48872
    86
      required: Dependencies, name: Document.Node.Name): Dependencies =
wenzelm@44615
    87
  {
wenzelm@48871
    88
    if (required.seen(name)) required
wenzelm@48871
    89
    else if (thy_load.loaded_theories(name.theory)) required + name
wenzelm@43651
    90
    else {
wenzelm@54549
    91
      def message: String =
wenzelm@54722
    92
        "The error(s) above occurred for theory " + quote(name.theory) + required_by(initiators)
wenzelm@50414
    93
wenzelm@43651
    94
      try {
wenzelm@44615
    95
        if (initiators.contains(name)) error(cycle_msg(initiators))
wenzelm@51294
    96
        val header =
wenzelm@54549
    97
          try { thy_load.check_thy(name).cat_errors(message) }
wenzelm@54549
    98
          catch { case ERROR(msg) => cat_error(msg, message) }
wenzelm@51294
    99
        Dep(name, header) :: require_thys(name :: initiators, required + name, header.imports)
wenzelm@43651
   100
      }
wenzelm@48707
   101
      catch {
wenzelm@48707
   102
        case e: Throwable =>
wenzelm@51294
   103
          Dep(name, Document.Node.bad_header(Exn.message(e))) :: (required + name)
wenzelm@48707
   104
      }
wenzelm@43651
   105
    }
wenzelm@43651
   106
  }
wenzelm@43651
   107
wenzelm@51294
   108
  def dependencies(names: List[Document.Node.Name]): Dependencies =
wenzelm@51294
   109
    require_thys(Nil, Dependencies.empty, names)
wenzelm@43651
   110
}