src/Pure/Tools/build.scala
changeset 56801 8dd9df88f647
parent 56782 433cf57550fa
child 56824 5ae68f53b7c2
     1.1 --- a/src/Pure/Tools/build.scala	Wed Apr 30 13:11:24 2014 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Wed Apr 30 22:34:11 2014 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4      parent: Option[String],
     1.5      description: String,
     1.6      options: List[Options.Spec],
     1.7 -    theories: List[(List[Options.Spec], List[String])],
     1.8 +    theories: List[(Boolean, List[Options.Spec], List[String])],
     1.9      files: List[String],
    1.10      document_files: List[(String, String)]) extends Entry
    1.11  
    1.12 @@ -70,7 +70,7 @@
    1.13      parent: Option[String],
    1.14      description: String,
    1.15      options: Options,
    1.16 -    theories: List[(Options, List[Path])],
    1.17 +    theories: List[(Boolean, Options, List[Path])],
    1.18      files: List[Path],
    1.19      document_files: List[(Path, Path)],
    1.20      entry_digest: SHA1.Digest)
    1.21 @@ -89,8 +89,8 @@
    1.22        val session_options = options ++ entry.options
    1.23  
    1.24        val theories =
    1.25 -        entry.theories.map({ case (opts, thys) =>
    1.26 -          (session_options ++ opts, thys.map(Path.explode(_))) })
    1.27 +        entry.theories.map({ case (global, opts, thys) =>
    1.28 +          (global, session_options ++ opts, thys.map(Path.explode(_))) })
    1.29        val files = entry.files.map(Path.explode(_))
    1.30        val document_files =
    1.31          entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
    1.32 @@ -179,8 +179,8 @@
    1.33          if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
    1.34          else pre_selected
    1.35  
    1.36 -      val tree1 = new Session_Tree(graph.restrict(graph.all_preds(selected).toSet))
    1.37 -      (selected, tree1)
    1.38 +      val graph1 = graph.restrict(graph.all_preds(selected).toSet)
    1.39 +      (selected, new Session_Tree(graph1))
    1.40      }
    1.41  
    1.42      def topological_order: List[(String, Session_Info)] =
    1.43 @@ -199,6 +199,7 @@
    1.44    private val IN = "in"
    1.45    private val DESCRIPTION = "description"
    1.46    private val OPTIONS = "options"
    1.47 +  private val GLOBAL_THEORIES = "global_theories"
    1.48    private val THEORIES = "theories"
    1.49    private val FILES = "files"
    1.50    private val DOCUMENT_FILES = "document_files"
    1.51 @@ -206,7 +207,7 @@
    1.52    lazy val root_syntax =
    1.53      Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
    1.54        (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
    1.55 -      IN + DESCRIPTION + OPTIONS + THEORIES + FILES + DOCUMENT_FILES
    1.56 +      IN + DESCRIPTION + OPTIONS + GLOBAL_THEORIES + THEORIES + FILES + DOCUMENT_FILES
    1.57  
    1.58    object Parser extends Parse.Parser
    1.59    {
    1.60 @@ -226,8 +227,9 @@
    1.61        val options = keyword("[") ~> rep1sep(option, keyword(",")) <~ keyword("]")
    1.62  
    1.63        val theories =
    1.64 -        keyword(THEORIES) ~! ((options | success(Nil)) ~ rep(theory_name)) ^^
    1.65 -          { case _ ~ (x ~ y) => (x, y) }
    1.66 +        (keyword(GLOBAL_THEORIES) | keyword(THEORIES)) ~!
    1.67 +          ((options | success(Nil)) ~ rep(theory_xname)) ^^
    1.68 +          { case x ~ (y ~ z) => (x == GLOBAL_THEORIES, y, z) }
    1.69  
    1.70        val document_files =
    1.71          keyword(DOCUMENT_FILES) ~!
    1.72 @@ -407,6 +409,7 @@
    1.73  
    1.74    sealed case class Session_Content(
    1.75      loaded_theories: Set[String],
    1.76 +    known_theories: Map[String, Document.Node.Name],
    1.77      keywords: Thy_Header.Keywords,
    1.78      syntax: Outer_Syntax,
    1.79      sources: List[(Path, SHA1.Digest)])
    1.80 @@ -425,15 +428,14 @@
    1.81            if (progress.stopped) throw Exn.Interrupt()
    1.82  
    1.83            try {
    1.84 -            val (preloaded, parent_syntax) =
    1.85 -              info.parent match {
    1.86 +            val (loaded_theories0, known_theories0, syntax0) =
    1.87 +              info.parent.map(deps(_)) match {
    1.88                  case None =>
    1.89 -                  (Set.empty[String], Outer_Syntax.init())
    1.90 -                case Some(parent_name) =>
    1.91 -                  val parent = deps(parent_name)
    1.92 -                  (parent.loaded_theories, parent.syntax)
    1.93 +                  (Set.empty[String], Map.empty[String, Document.Node.Name], Outer_Syntax.init())
    1.94 +                case Some(parent) =>
    1.95 +                  (parent.loaded_theories, parent.known_theories, parent.syntax)
    1.96                }
    1.97 -            val resources = new Resources(preloaded, parent_syntax)
    1.98 +            val resources = new Resources(loaded_theories0, known_theories0, syntax0)
    1.99              val thy_info = new Thy_Info(resources)
   1.100  
   1.101              if (verbose || list_files) {
   1.102 @@ -444,15 +446,33 @@
   1.103              }
   1.104  
   1.105              val thy_deps =
   1.106 -              thy_info.dependencies(
   1.107 -                info.theories.map(_._2).flatten.
   1.108 -                  map(thy => (resources.node_name(info.dir + Resources.thy_path(thy)), info.pos)))
   1.109 +            {
   1.110 +              val root_theories =
   1.111 +                info.theories.flatMap({
   1.112 +                  case (global, _, thys) =>
   1.113 +                    thys.map(thy =>
   1.114 +                      (resources.node_name(
   1.115 +                        if (global) "" else name, info.dir + Resources.thy_path(thy)), info.pos))
   1.116 +                })
   1.117 +              val thy_deps = thy_info.dependencies(name, root_theories)
   1.118  
   1.119 -            thy_deps.errors match {
   1.120 -              case Nil =>
   1.121 -              case errs => error(cat_lines(errs))
   1.122 +              thy_deps.errors match {
   1.123 +                case Nil => thy_deps
   1.124 +                case errs => error(cat_lines(errs))
   1.125 +              }
   1.126              }
   1.127  
   1.128 +            val known_theories =
   1.129 +              (known_theories0 /: thy_deps.deps)({ case (known, dep) =>
   1.130 +                val name = dep.name
   1.131 +                known.get(name.theory) match {
   1.132 +                  case Some(name1) if name != name1 =>
   1.133 +                    error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node))
   1.134 +                  case _ =>
   1.135 +                    known + (name.theory -> name) + (Long_Name.base_name(name.theory) -> name)
   1.136 +                }
   1.137 +              })
   1.138 +
   1.139              val loaded_theories = thy_deps.loaded_theories
   1.140              val keywords = thy_deps.keywords
   1.141              val syntax = thy_deps.syntax.asInstanceOf[Outer_Syntax]
   1.142 @@ -480,7 +500,9 @@
   1.143  
   1.144              val sources = all_files.map(p => (p, SHA1.digest(p.file)))
   1.145  
   1.146 -            deps + (name -> Session_Content(loaded_theories, keywords, syntax, sources))
   1.147 +            val content =
   1.148 +              Session_Content(loaded_theories, known_theories, keywords, syntax, sources)
   1.149 +            deps + (name -> content)
   1.150            }
   1.151            catch {
   1.152              case ERROR(msg) =>
   1.153 @@ -528,12 +550,13 @@
   1.154        if (is_pure(name)) Options.encode(info.options)
   1.155        else
   1.156          {
   1.157 +          val theories = info.theories.map(x => (x._2, x._3))
   1.158            import XML.Encode._
   1.159                pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode,
   1.160                  pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string,
   1.161                    list(pair(Options.encode, list(Path.encode))))))))))))(
   1.162                (command_timings, (do_output, (info.options, (verbose, (browser_info,
   1.163 -                (info.document_files, (parent, (info.chapter, (name, info.theories))))))))))
   1.164 +                (info.document_files, (parent, (info.chapter, (name, theories))))))))))
   1.165          }))
   1.166  
   1.167      private val env =