discontinued obsolete 'files' in session ROOT;
authorwenzelm
Mon Oct 02 19:58:29 2017 +0200 (20 months ago)
changeset 66759918f15c9367a
parent 66758 9312ce5a938d
child 66760 d44ea023ac09
discontinued obsolete 'files' in session ROOT;
NEWS
src/Doc/System/Sessions.thy
src/Pure/Thy/sessions.scala
     1.1 --- a/NEWS	Mon Oct 02 19:38:39 2017 +0200
     1.2 +++ b/NEWS	Mon Oct 02 19:58:29 2017 +0200
     1.3 @@ -18,6 +18,10 @@
     1.4  file name, such that the Isabelle build process knows about it, but
     1.5  without specific Prover IDE management.
     1.6  
     1.7 +* Session ROOT entries no longer allow specification of 'files'. Rare
     1.8 +INCOMPATIBILITY, use command 'external_file' within a proper theory
     1.9 +context.
    1.10 +
    1.11  
    1.12  *** HOL ***
    1.13  
     2.1 --- a/src/Doc/System/Sessions.thy	Mon Oct 02 19:38:39 2017 +0200
     2.2 +++ b/src/Doc/System/Sessions.thy	Mon Oct 02 19:58:29 2017 +0200
     2.3 @@ -54,7 +54,7 @@
     2.4  
     2.5      @{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body
     2.6      ;
     2.7 -    body: description? options? (theories+) \<newline> files? (document_files*)
     2.8 +    body: description? options? (theories+) \<newline> (document_files*)
     2.9      ;
    2.10      spec: @{syntax name} groups? dir?
    2.11      ;
    2.12 @@ -76,16 +76,13 @@
    2.13      ;
    2.14      theory_entry: @{syntax name} ('(' @'global' ')')?
    2.15      ;
    2.16 -    files: @'files' (@{syntax name}+)
    2.17 -    ;
    2.18      document_files: @'document_files' ('(' dir ')')? (@{syntax name}+)
    2.19    \<close>}
    2.20  
    2.21    \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on
    2.22 -  parent session \<open>B\<close>, with its content given in \<open>body\<close> (imported sessions,
    2.23 -  theories and auxiliary source files). Note that a parent (like \<open>HOL\<close>) is
    2.24 -  mandatory in practical applications: only Isabelle/Pure can bootstrap itself
    2.25 -  from nothing.
    2.26 +  parent session \<open>B\<close>, with its content given in \<open>body\<close> (imported sessions and
    2.27 +  theories). Note that a parent (like \<open>HOL\<close>) is mandatory in practical
    2.28 +  applications: only Isabelle/Pure can bootstrap itself from nothing.
    2.29  
    2.30    All such session specifications together describe a hierarchy (graph) of
    2.31    sessions, with globally unique names. The new session name \<open>A\<close> should be
    2.32 @@ -103,9 +100,8 @@
    2.33    directory for this session; by default this is the current directory of the
    2.34    \<^verbatim>\<open>ROOT\<close> file.
    2.35  
    2.36 -  All theories and auxiliary source files are located relatively to the
    2.37 -  session directory. The prover process is run within the same as its current
    2.38 -  working directory.
    2.39 +  All theory files are located relatively to the session directory. The prover
    2.40 +  process is run within the same as its current working directory.
    2.41  
    2.42    \<^descr> \isakeyword{description}~\<open>text\<close> is a free-form annotation for this
    2.43    session.
    2.44 @@ -135,12 +131,6 @@
    2.45    the default is to qualify theory names by the session name, in order to
    2.46    ensure globally unique names in big session graphs.
    2.47  
    2.48 -  \<^descr> \isakeyword{files}~\<open>files\<close> lists additional source files that are involved
    2.49 -  in the processing of this session. This should cover anything outside the
    2.50 -  formal content of the theory sources. In contrast, files that are loaded
    2.51 -  formally within a theory, e.g.\ via @{command "ML_file"}, need not be
    2.52 -  declared again.
    2.53 -
    2.54    \<^descr> \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>base_dir) files\<close> lists
    2.55    source files for document preparation, typically \<^verbatim>\<open>.tex\<close> and \<^verbatim>\<open>.sty\<close> for
    2.56    {\LaTeX}. Only these explicitly given files are copied from the base
     3.1 --- a/src/Pure/Thy/sessions.scala	Mon Oct 02 19:38:39 2017 +0200
     3.2 +++ b/src/Pure/Thy/sessions.scala	Mon Oct 02 19:58:29 2017 +0200
     3.3 @@ -241,7 +241,6 @@
     3.4  
     3.5              val session_files =
     3.6                (theory_files ::: loaded_files.flatMap(_._2) :::
     3.7 -                info.files.map(file => info.dir + file) :::
     3.8                  info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
     3.9  
    3.10              val imported_files = if (inlined_files) thy_deps.imported_files else Nil
    3.11 @@ -367,7 +366,6 @@
    3.12      imports: List[String],
    3.13      theories: List[(Options, List[(String, Position.T)])],
    3.14      global_theories: List[String],
    3.15 -    files: List[Path],
    3.16      document_files: List[(Path, Path)],
    3.17      meta_digest: SHA1.Digest)
    3.18    {
    3.19 @@ -546,7 +544,6 @@
    3.20    private val SESSIONS = "sessions"
    3.21    private val THEORIES = "theories"
    3.22    private val GLOBAL = "global"
    3.23 -  private val FILES = "files"
    3.24    private val DOCUMENT_FILES = "document_files"
    3.25  
    3.26    lazy val root_syntax =
    3.27 @@ -557,7 +554,6 @@
    3.28        (OPTIONS, Keyword.QUASI_COMMAND) +
    3.29        (SESSIONS, Keyword.QUASI_COMMAND) +
    3.30        (THEORIES, Keyword.QUASI_COMMAND) +
    3.31 -      (FILES, Keyword.QUASI_COMMAND) +
    3.32        (DOCUMENT_FILES, Keyword.QUASI_COMMAND)
    3.33  
    3.34    private object Parser extends Parse.Parser with Options.Parser
    3.35 @@ -574,7 +570,6 @@
    3.36        options: List[Options.Spec],
    3.37        imports: List[String],
    3.38        theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
    3.39 -      files: List[String],
    3.40        document_files: List[(String, String)]) extends Entry
    3.41      {
    3.42        def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] =
    3.43 @@ -624,10 +619,9 @@
    3.44                (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
    3.45                (($$$(SESSIONS) ~! rep(session_name)  ^^ { case _ ~ x => x }) | success(Nil)) ~
    3.46                rep1(theories) ~
    3.47 -              (($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
    3.48                (rep(document_files) ^^ (x => x.flatten))))) ^^
    3.49 -        { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j))) =>
    3.50 -            Session_Entry(pos, a, b, c, d, e, f, g, h, i, j) }
    3.51 +        { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
    3.52 +            Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
    3.53      }
    3.54  
    3.55      def parse(options: Options, select: Boolean, dir: Path): List[(String, Info)] =
    3.56 @@ -656,18 +650,17 @@
    3.57                else thy_name
    3.58              }
    3.59  
    3.60 -          val files = entry.files.map(Path.explode(_))
    3.61            val document_files =
    3.62              entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
    3.63  
    3.64            val meta_digest =
    3.65              SHA1.digest((entry_chapter, name, entry.parent, entry.options, entry.imports,
    3.66 -              entry.theories_no_position, entry.files, entry.document_files).toString)
    3.67 +              entry.theories_no_position, entry.document_files).toString)
    3.68  
    3.69            val info =
    3.70              Info(name, entry_chapter, select, entry.pos, entry.groups,
    3.71                dir + Path.explode(entry.path), entry.parent, entry.description, session_options,
    3.72 -              entry.imports, theories, global_theories, files, document_files, meta_digest)
    3.73 +              entry.imports, theories, global_theories, document_files, meta_digest)
    3.74  
    3.75            (name, info)
    3.76          }