# HG changeset patch # User wenzelm # Date 1506967109 -7200 # Node ID 918f15c9367a2a1ed20c80e5791643ee9b017d05 # Parent 9312ce5a938df5217cd318f46a0f26951e86f133 discontinued obsolete 'files' in session ROOT; diff -r 9312ce5a938d -r 918f15c9367a NEWS --- a/NEWS Mon Oct 02 19:38:39 2017 +0200 +++ b/NEWS Mon Oct 02 19:58:29 2017 +0200 @@ -18,6 +18,10 @@ file name, such that the Isabelle build process knows about it, but without specific Prover IDE management. +* Session ROOT entries no longer allow specification of 'files'. Rare +INCOMPATIBILITY, use command 'external_file' within a proper theory +context. + *** HOL *** diff -r 9312ce5a938d -r 918f15c9367a src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Mon Oct 02 19:38:39 2017 +0200 +++ b/src/Doc/System/Sessions.thy Mon Oct 02 19:58:29 2017 +0200 @@ -54,7 +54,7 @@ @{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body ; - body: description? options? (theories+) \ files? (document_files*) + body: description? options? (theories+) \ (document_files*) ; spec: @{syntax name} groups? dir? ; @@ -76,16 +76,13 @@ ; theory_entry: @{syntax name} ('(' @'global' ')')? ; - files: @'files' (@{syntax name}+) - ; document_files: @'document_files' ('(' dir ')')? (@{syntax name}+) \} \<^descr> \isakeyword{session}~\A = B + body\ defines a new session \A\ based on - parent session \B\, with its content given in \body\ (imported sessions, - theories and auxiliary source files). Note that a parent (like \HOL\) is - mandatory in practical applications: only Isabelle/Pure can bootstrap itself - from nothing. + parent session \B\, with its content given in \body\ (imported sessions and + theories). Note that a parent (like \HOL\) is mandatory in practical + applications: only Isabelle/Pure can bootstrap itself from nothing. All such session specifications together describe a hierarchy (graph) of sessions, with globally unique names. The new session name \A\ should be @@ -103,9 +100,8 @@ directory for this session; by default this is the current directory of the \<^verbatim>\ROOT\ file. - All theories and auxiliary source files are located relatively to the - session directory. The prover process is run within the same as its current - working directory. + All theory files are located relatively to the session directory. The prover + process is run within the same as its current working directory. \<^descr> \isakeyword{description}~\text\ is a free-form annotation for this session. @@ -135,12 +131,6 @@ the default is to qualify theory names by the session name, in order to ensure globally unique names in big session graphs. - \<^descr> \isakeyword{files}~\files\ lists additional source files that are involved - in the processing of this session. This should cover anything outside the - formal content of the theory sources. In contrast, files that are loaded - formally within a theory, e.g.\ via @{command "ML_file"}, need not be - declared again. - \<^descr> \isakeyword{document_files}~\(\\isakeyword{in}~\base_dir) files\ lists source files for document preparation, typically \<^verbatim>\.tex\ and \<^verbatim>\.sty\ for {\LaTeX}. Only these explicitly given files are copied from the base diff -r 9312ce5a938d -r 918f15c9367a src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Mon Oct 02 19:38:39 2017 +0200 +++ b/src/Pure/Thy/sessions.scala Mon Oct 02 19:58:29 2017 +0200 @@ -241,7 +241,6 @@ val session_files = (theory_files ::: loaded_files.flatMap(_._2) ::: - info.files.map(file => info.dir + file) ::: info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand) val imported_files = if (inlined_files) thy_deps.imported_files else Nil @@ -367,7 +366,6 @@ imports: List[String], theories: List[(Options, List[(String, Position.T)])], global_theories: List[String], - files: List[Path], document_files: List[(Path, Path)], meta_digest: SHA1.Digest) { @@ -546,7 +544,6 @@ private val SESSIONS = "sessions" private val THEORIES = "theories" private val GLOBAL = "global" - private val FILES = "files" private val DOCUMENT_FILES = "document_files" lazy val root_syntax = @@ -557,7 +554,6 @@ (OPTIONS, Keyword.QUASI_COMMAND) + (SESSIONS, Keyword.QUASI_COMMAND) + (THEORIES, Keyword.QUASI_COMMAND) + - (FILES, Keyword.QUASI_COMMAND) + (DOCUMENT_FILES, Keyword.QUASI_COMMAND) private object Parser extends Parse.Parser with Options.Parser @@ -574,7 +570,6 @@ options: List[Options.Spec], imports: List[String], theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])], - files: List[String], document_files: List[(String, String)]) extends Entry { def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] = @@ -624,10 +619,9 @@ (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~ (($$$(SESSIONS) ~! rep(session_name) ^^ { case _ ~ x => x }) | success(Nil)) ~ rep1(theories) ~ - (($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~ (rep(document_files) ^^ (x => x.flatten))))) ^^ - { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j))) => - Session_Entry(pos, a, b, c, d, e, f, g, h, i, j) } + { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) => + Session_Entry(pos, a, b, c, d, e, f, g, h, i) } } def parse(options: Options, select: Boolean, dir: Path): List[(String, Info)] = @@ -656,18 +650,17 @@ else thy_name } - val files = entry.files.map(Path.explode(_)) val document_files = entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) }) val meta_digest = SHA1.digest((entry_chapter, name, entry.parent, entry.options, entry.imports, - entry.theories_no_position, entry.files, entry.document_files).toString) + entry.theories_no_position, entry.document_files).toString) val info = Info(name, entry_chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path), entry.parent, entry.description, session_options, - entry.imports, theories, global_theories, files, document_files, meta_digest) + entry.imports, theories, global_theories, document_files, meta_digest) (name, info) }