src/Pure/Tools/build.scala
changeset 56533 cd8b6d849b6a
parent 56464 555f4be59be6
child 56667 65e84b0ef974
     1.1 --- a/src/Pure/Tools/build.scala	Fri Apr 11 09:36:38 2014 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Fri Apr 11 11:52:28 2014 +0200
     1.3 @@ -58,7 +58,8 @@
     1.4      description: String,
     1.5      options: List[Options.Spec],
     1.6      theories: List[(List[Options.Spec], List[String])],
     1.7 -    files: List[String]) extends Entry
     1.8 +    files: List[String],
     1.9 +    document_files: List[(String, String)]) extends Entry
    1.10  
    1.11    // internal version
    1.12    sealed case class Session_Info(
    1.13 @@ -72,6 +73,7 @@
    1.14      options: Options,
    1.15      theories: List[(Options, List[Path])],
    1.16      files: List[Path],
    1.17 +    document_files: List[(Path, Path)],
    1.18      entry_digest: SHA1.Digest)
    1.19  
    1.20    def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
    1.21 @@ -91,12 +93,17 @@
    1.22          entry.theories.map({ case (opts, thys) =>
    1.23            (session_options ++ opts, thys.map(Path.explode(_))) })
    1.24        val files = entry.files.map(Path.explode(_))
    1.25 +      val document_files =
    1.26 +        entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
    1.27 +
    1.28        val entry_digest =
    1.29 -        SHA1.digest((chapter, name, entry.parent, entry.options, entry.theories).toString)
    1.30 +        SHA1.digest((chapter, name, entry.parent, entry.options,
    1.31 +          entry.theories, entry.files, entry.document_files).toString)
    1.32  
    1.33        val info =
    1.34          Session_Info(chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path),
    1.35 -          entry.parent, entry.description, session_options, theories, files, entry_digest)
    1.36 +          entry.parent, entry.description, session_options, theories, files,
    1.37 +          document_files, entry_digest)
    1.38  
    1.39        (name, info)
    1.40      }
    1.41 @@ -195,11 +202,12 @@
    1.42    private val OPTIONS = "options"
    1.43    private val THEORIES = "theories"
    1.44    private val FILES = "files"
    1.45 +  private val DOCUMENT_FILES = "document_files"
    1.46  
    1.47    lazy val root_syntax =
    1.48      Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
    1.49        (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
    1.50 -      IN + DESCRIPTION + OPTIONS + THEORIES + FILES
    1.51 +      IN + DESCRIPTION + OPTIONS + THEORIES + FILES + DOCUMENT_FILES
    1.52  
    1.53    private object Parser extends Parse.Parser
    1.54    {
    1.55 @@ -222,6 +230,12 @@
    1.56          keyword(THEORIES) ~! ((options | success(Nil)) ~ rep(theory_name)) ^^
    1.57            { case _ ~ (x ~ y) => (x, y) }
    1.58  
    1.59 +      val document_files =
    1.60 +        keyword(DOCUMENT_FILES) ~!
    1.61 +          ((keyword("(") ~! (keyword(IN) ~! (path ~ keyword(")"))) ^^
    1.62 +              { case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~
    1.63 +            rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
    1.64 +
    1.65        command(SESSION) ~!
    1.66          (session_name ~
    1.67            ((keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
    1.68 @@ -231,9 +245,10 @@
    1.69                ((keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
    1.70                ((keyword(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
    1.71                rep1(theories) ~
    1.72 -              ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil))))) ^^
    1.73 -        { case pos ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h))) =>
    1.74 -            Session_Entry(pos, a, b, c, d, e, f, g, h) }
    1.75 +              ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
    1.76 +              (rep(document_files) ^^ (x => x.flatten))))) ^^
    1.77 +        { case pos ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
    1.78 +            Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
    1.79      }
    1.80  
    1.81      def parse_entries(root: Path): List[(String, Session_Entry)] =
    1.82 @@ -445,7 +460,8 @@
    1.83  
    1.84              val all_files =
    1.85                (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: loaded_files :::
    1.86 -                info.files.map(file => info.dir + file)).map(_.expand)
    1.87 +                info.files.map(file => info.dir + file) :::
    1.88 +                info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
    1.89  
    1.90              if (list_files) {
    1.91                progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
    1.92 @@ -513,10 +529,10 @@
    1.93          {
    1.94            import XML.Encode._
    1.95                pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode,
    1.96 -                pair(string, pair(string, pair(string,
    1.97 -                  list(pair(Options.encode, list(Path.encode)))))))))))(
    1.98 +                pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string,
    1.99 +                  list(pair(Options.encode, list(Path.encode))))))))))))(
   1.100                (command_timings, (do_output, (info.options, (verbose, (browser_info,
   1.101 -                (parent, (info.chapter, (name, info.theories)))))))))
   1.102 +                (info.document_files, (parent, (info.chapter, (name, info.theories))))))))))
   1.103          }))
   1.104  
   1.105      private val env =