some documentation;
authorwenzelm
Tue Apr 18 14:51:46 2017 +0200 (2017-04-18)
changeset 65504b80477da30eb
parent 65503 a3fffad8f217
child 65505 741fad555d82
some documentation;
NEWS
src/Doc/System/Sessions.thy
     1.1 --- a/NEWS	Tue Apr 18 14:19:49 2017 +0200
     1.2 +++ b/NEWS	Tue Apr 18 14:51:46 2017 +0200
     1.3 @@ -9,6 +9,13 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Theory names are qualified by the session name that they belong to.
     1.8 +This affects imports, but not the theory name space prefix: it remains
     1.9 +the theory base name as before. In order to import theories from other
    1.10 +sessions, the ROOT file format provides a new 'sessions' keyword. In
    1.11 +contrast, a theory that is imported in the old-fashioned manner via an
    1.12 +explicit file-system path belongs to the current session.
    1.13 +
    1.14  * The main theory entry points for some non-HOL sessions have changed,
    1.15  to avoid confusion with the global name "Main" of the session HOL. This
    1.16  leads to the follow renamings:
     2.1 --- a/src/Doc/System/Sessions.thy	Tue Apr 18 14:19:49 2017 +0200
     2.2 +++ b/src/Doc/System/Sessions.thy	Tue Apr 18 14:51:46 2017 +0200
     2.3 @@ -70,21 +70,24 @@
     2.4      ;
     2.5      value: @{syntax name} | @{syntax real}
     2.6      ;
     2.7 -    theory_entry: @{syntax name} ('(' @'global' ')')?
     2.8 +    sessions: @'sessions' (@{syntax name}+)
     2.9      ;
    2.10      theories: @'theories' opts? (theory_entry*)
    2.11      ;
    2.12 +    theory_entry: @{syntax name} ('(' @'global' ')')?
    2.13 +    ;
    2.14      files: @'files' (@{syntax name}+)
    2.15      ;
    2.16      document_files: @'document_files' ('(' dir ')')? (@{syntax name}+)
    2.17    \<close>}
    2.18  
    2.19    \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on
    2.20 -  parent session \<open>B\<close>, with its content given in \<open>body\<close> (theories and auxiliary
    2.21 -  source files). Note that a parent (like \<open>HOL\<close>) is mandatory in practical
    2.22 -  applications: only Isabelle/Pure can bootstrap itself from nothing.
    2.23 +  parent session \<open>B\<close>, with its content given in \<open>body\<close> (imported sessions,
    2.24 +  theories and auxiliary source files). Note that a parent (like \<open>HOL\<close>) is
    2.25 +  mandatory in practical applications: only Isabelle/Pure can bootstrap itself
    2.26 +  from nothing.
    2.27  
    2.28 -  All such session specifications together describe a hierarchy (tree) of
    2.29 +  All such session specifications together describe a hierarchy (graph) of
    2.30    sessions, with globally unique names. The new session name \<open>A\<close> should be
    2.31    sufficiently long and descriptive to stand on its own in a potentially large
    2.32    library.
    2.33 @@ -112,6 +115,12 @@
    2.34    but \<^emph>\<open>without\<close> propagation to child sessions. Note that \<open>z\<close> abbreviates \<open>z =
    2.35    true\<close> for Boolean options.
    2.36  
    2.37 +  \<^descr> \isakeyword{sessions}~\<open>names\<close> specifies sessions that are \<^emph>\<open>imported\<close> into
    2.38 +  the current name space of theories. This allows to refer to a theory \<open>A\<close>
    2.39 +  from session \<open>B\<close> by the qualified name \<open>B.A\<close> --- although it is loaded again
    2.40 +  into the current ML process, which is in contrast to a theory that is
    2.41 +  already present in the \<^emph>\<open>parent\<close> session.
    2.42 +
    2.43    \<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a block of theories that
    2.44    are processed within an environment that is augmented by the given options,
    2.45    in addition to the global session options given before. Any number of blocks
    2.46 @@ -121,7 +130,7 @@
    2.47    A theory name that is followed by \<open>(\<close>\isakeyword{global}\<open>)\<close> is treated
    2.48    literally in other session specifications or theory imports. In contrast,
    2.49    the default is to qualify theory names by the session name, in order to
    2.50 -  ensure globally unique names in big session trees.
    2.51 +  ensure globally unique names in big session graphs.
    2.52  
    2.53    \<^descr> \isakeyword{files}~\<open>files\<close> lists additional source files that are involved
    2.54    in the processing of this session. This should cover anything outside the