src/Pure/Thy/sessions.scala
changeset 69671 2486792eaf61
parent 69560 195371990820
child 69762 58fb0d779583
     1.1 --- a/src/Pure/Thy/sessions.scala	Wed Jan 16 17:12:48 2019 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Wed Jan 16 17:55:26 2019 +0100
     1.3 @@ -515,7 +515,7 @@
     1.4      theories: List[(Options, List[(String, Position.T)])],
     1.5      global_theories: List[String],
     1.6      document_files: List[(Path, Path)],
     1.7 -    export_files: List[(Path, List[String])],
     1.8 +    export_files: List[(Path, Int, List[String])],
     1.9      meta_digest: SHA1.Digest)
    1.10    {
    1.11      def deps: List[String] = parent.toList ::: imports
    1.12 @@ -568,7 +568,7 @@
    1.13          entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
    1.14  
    1.15        val export_files =
    1.16 -        entry.export_files.map({ case (dir, pats) => (Path.explode(dir), pats) })
    1.17 +        entry.export_files.map({ case (dir, prune, pats) => (Path.explode(dir), prune, pats) })
    1.18  
    1.19        val meta_digest =
    1.20          SHA1.digest((name, chapter, entry.parent, entry.options, entry.imports,
    1.21 @@ -831,7 +831,7 @@
    1.22      imports: List[String],
    1.23      theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
    1.24      document_files: List[(String, String)],
    1.25 -    export_files: List[(String, List[String])]) extends Entry
    1.26 +    export_files: List[(String, Int, List[String])]) extends Entry
    1.27    {
    1.28      def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] =
    1.29        theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) })
    1.30 @@ -870,9 +870,11 @@
    1.31          $$$(DOCUMENT_FILES) ~!
    1.32            ((in_path | success("document")) ~ rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
    1.33  
    1.34 +      val prune = $$$("[") ~! (nat ~ $$$("]")) ^^ { case _ ~ (x ~ _) => x } | success(0)
    1.35 +
    1.36        val export_files =
    1.37 -        $$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ rep1(embedded)) ^^
    1.38 -          { case _ ~ (x ~ y) => (x, y) }
    1.39 +        $$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ prune ~ rep1(embedded)) ^^
    1.40 +          { case _ ~ (x ~ y ~ z) => (x, y, z) }
    1.41  
    1.42        command(SESSION) ~!
    1.43          (position(session_name) ~