src/Pure/Thy/sessions.scala
changeset 66759 918f15c9367a
parent 66749 0445cfaf6132
child 66764 006deaf5c3dc
     1.1 --- a/src/Pure/Thy/sessions.scala	Mon Oct 02 19:38:39 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Mon Oct 02 19:58:29 2017 +0200
     1.3 @@ -241,7 +241,6 @@
     1.4  
     1.5              val session_files =
     1.6                (theory_files ::: loaded_files.flatMap(_._2) :::
     1.7 -                info.files.map(file => info.dir + file) :::
     1.8                  info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
     1.9  
    1.10              val imported_files = if (inlined_files) thy_deps.imported_files else Nil
    1.11 @@ -367,7 +366,6 @@
    1.12      imports: List[String],
    1.13      theories: List[(Options, List[(String, Position.T)])],
    1.14      global_theories: List[String],
    1.15 -    files: List[Path],
    1.16      document_files: List[(Path, Path)],
    1.17      meta_digest: SHA1.Digest)
    1.18    {
    1.19 @@ -546,7 +544,6 @@
    1.20    private val SESSIONS = "sessions"
    1.21    private val THEORIES = "theories"
    1.22    private val GLOBAL = "global"
    1.23 -  private val FILES = "files"
    1.24    private val DOCUMENT_FILES = "document_files"
    1.25  
    1.26    lazy val root_syntax =
    1.27 @@ -557,7 +554,6 @@
    1.28        (OPTIONS, Keyword.QUASI_COMMAND) +
    1.29        (SESSIONS, Keyword.QUASI_COMMAND) +
    1.30        (THEORIES, Keyword.QUASI_COMMAND) +
    1.31 -      (FILES, Keyword.QUASI_COMMAND) +
    1.32        (DOCUMENT_FILES, Keyword.QUASI_COMMAND)
    1.33  
    1.34    private object Parser extends Parse.Parser with Options.Parser
    1.35 @@ -574,7 +570,6 @@
    1.36        options: List[Options.Spec],
    1.37        imports: List[String],
    1.38        theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
    1.39 -      files: List[String],
    1.40        document_files: List[(String, String)]) extends Entry
    1.41      {
    1.42        def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] =
    1.43 @@ -624,10 +619,9 @@
    1.44                (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
    1.45                (($$$(SESSIONS) ~! rep(session_name)  ^^ { case _ ~ x => x }) | success(Nil)) ~
    1.46                rep1(theories) ~
    1.47 -              (($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
    1.48                (rep(document_files) ^^ (x => x.flatten))))) ^^
    1.49 -        { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j))) =>
    1.50 -            Session_Entry(pos, a, b, c, d, e, f, g, h, i, j) }
    1.51 +        { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
    1.52 +            Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
    1.53      }
    1.54  
    1.55      def parse(options: Options, select: Boolean, dir: Path): List[(String, Info)] =
    1.56 @@ -656,18 +650,17 @@
    1.57                else thy_name
    1.58              }
    1.59  
    1.60 -          val files = entry.files.map(Path.explode(_))
    1.61            val document_files =
    1.62              entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
    1.63  
    1.64            val meta_digest =
    1.65              SHA1.digest((entry_chapter, name, entry.parent, entry.options, entry.imports,
    1.66 -              entry.theories_no_position, entry.files, entry.document_files).toString)
    1.67 +              entry.theories_no_position, entry.document_files).toString)
    1.68  
    1.69            val info =
    1.70              Info(name, entry_chapter, select, entry.pos, entry.groups,
    1.71                dir + Path.explode(entry.path), entry.parent, entry.description, session_options,
    1.72 -              entry.imports, theories, global_theories, files, document_files, meta_digest)
    1.73 +              entry.imports, theories, global_theories, document_files, meta_digest)
    1.74  
    1.75            (name, info)
    1.76          }