src/Doc/System/Sessions.thy
changeset 66759 918f15c9367a
parent 66748 3efac90a11a7
child 66841 5c32a072ca8b
     1.1 --- a/src/Doc/System/Sessions.thy	Mon Oct 02 19:38:39 2017 +0200
     1.2 +++ b/src/Doc/System/Sessions.thy	Mon Oct 02 19:58:29 2017 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4  
     1.5      @{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body
     1.6      ;
     1.7 -    body: description? options? (theories+) \<newline> files? (document_files*)
     1.8 +    body: description? options? (theories+) \<newline> (document_files*)
     1.9      ;
    1.10      spec: @{syntax name} groups? dir?
    1.11      ;
    1.12 @@ -76,16 +76,13 @@
    1.13      ;
    1.14      theory_entry: @{syntax name} ('(' @'global' ')')?
    1.15      ;
    1.16 -    files: @'files' (@{syntax name}+)
    1.17 -    ;
    1.18      document_files: @'document_files' ('(' dir ')')? (@{syntax name}+)
    1.19    \<close>}
    1.20  
    1.21    \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on
    1.22 -  parent session \<open>B\<close>, with its content given in \<open>body\<close> (imported sessions,
    1.23 -  theories and auxiliary source files). Note that a parent (like \<open>HOL\<close>) is
    1.24 -  mandatory in practical applications: only Isabelle/Pure can bootstrap itself
    1.25 -  from nothing.
    1.26 +  parent session \<open>B\<close>, with its content given in \<open>body\<close> (imported sessions and
    1.27 +  theories). Note that a parent (like \<open>HOL\<close>) is mandatory in practical
    1.28 +  applications: only Isabelle/Pure can bootstrap itself from nothing.
    1.29  
    1.30    All such session specifications together describe a hierarchy (graph) of
    1.31    sessions, with globally unique names. The new session name \<open>A\<close> should be
    1.32 @@ -103,9 +100,8 @@
    1.33    directory for this session; by default this is the current directory of the
    1.34    \<^verbatim>\<open>ROOT\<close> file.
    1.35  
    1.36 -  All theories and auxiliary source files are located relatively to the
    1.37 -  session directory. The prover process is run within the same as its current
    1.38 -  working directory.
    1.39 +  All theory files are located relatively to the session directory. The prover
    1.40 +  process is run within the same as its current working directory.
    1.41  
    1.42    \<^descr> \isakeyword{description}~\<open>text\<close> is a free-form annotation for this
    1.43    session.
    1.44 @@ -135,12 +131,6 @@
    1.45    the default is to qualify theory names by the session name, in order to
    1.46    ensure globally unique names in big session graphs.
    1.47  
    1.48 -  \<^descr> \isakeyword{files}~\<open>files\<close> lists additional source files that are involved
    1.49 -  in the processing of this session. This should cover anything outside the
    1.50 -  formal content of the theory sources. In contrast, files that are loaded
    1.51 -  formally within a theory, e.g.\ via @{command "ML_file"}, need not be
    1.52 -  declared again.
    1.53 -
    1.54    \<^descr> \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>base_dir) files\<close> lists
    1.55    source files for document preparation, typically \<^verbatim>\<open>.tex\<close> and \<^verbatim>\<open>.sty\<close> for
    1.56    {\LaTeX}. Only these explicitly given files are copied from the base