--- 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+) \<newline> files? (document_files*)
+ body: description? options? (theories+) \<newline> (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}+)
\<close>}
\<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on
- parent session \<open>B\<close>, with its content given in \<open>body\<close> (imported sessions,
- theories and auxiliary source files). Note that a parent (like \<open>HOL\<close>) is
- mandatory in practical applications: only Isabelle/Pure can bootstrap itself
- from nothing.
+ parent session \<open>B\<close>, with its content given in \<open>body\<close> (imported sessions and
+ theories). Note that a parent (like \<open>HOL\<close>) 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 \<open>A\<close> should be
@@ -103,9 +100,8 @@
directory for this session; by default this is the current directory of the
\<^verbatim>\<open>ROOT\<close> 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}~\<open>text\<close> 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}~\<open>files\<close> 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}~\<open>(\<close>\isakeyword{in}~\<open>base_dir) files\<close> lists
source files for document preparation, typically \<^verbatim>\<open>.tex\<close> and \<^verbatim>\<open>.sty\<close> for
{\LaTeX}. Only these explicitly given files are copied from the base
--- 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)
}