--- a/NEWS Sun Sep 08 16:49:32 2019 +0200
+++ b/NEWS Sun Sep 08 17:15:46 2019 +0200
@@ -9,6 +9,11 @@
*** General ***
+* Session ROOT files need to specify explicit 'directories' for import
+of theory files. Directories that are used by different sessions should
+be avoided, but may be specified as 'overlapping' (this affects formal
+theory names in the Prover IDE).
+
* Internal derivations record dependencies on oracles and other theorems
accurately, including the implicit type-class reasoning wrt. proven
class relations and type arities. In particular, the formal tagging with
--- a/src/Doc/System/Sessions.thy Sun Sep 08 16:49:32 2019 +0200
+++ b/src/Doc/System/Sessions.thy Sun Sep 08 17:15:46 2019 +0200
@@ -53,8 +53,9 @@
;
@{syntax_def session_entry}: @'session' @{syntax system_name} groups? dir? '=' \<newline>
- (@{syntax system_name} '+')? description? options? \<newline>
- (sessions?) (theories*) (document_files*) \<newline> (export_files*)
+ (@{syntax system_name} '+')? description? directories? \<newline>
+ options? (sessions?) (theories*) (document_files*) \<newline>
+ (export_files*)
;
groups: '(' (@{syntax name} +) ')'
;
@@ -62,6 +63,8 @@
;
description: @'description' @{syntax text}
;
+ directories: @'directories' ((dir ('(' @'overlapping' ')')?) +)
+ ;
options: @'options' opts
;
opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']'
@@ -107,6 +110,16 @@
\<^descr> \isakeyword{description}~\<open>text\<close> is a free-form annotation for this
session.
+ \<^descr> \isakeyword{directories}~\<open>dirs\<close> specifies additional directories for
+ import of theory files via \isakeyword{theories} within \<^verbatim>\<open>ROOT\<close> or
+ \<^theory_text>\<open>imports\<close> within a theory; \<open>dirs\<close> are relative to the main session
+ directory (cf.\ \isakeyword{session} \dots \isakeyword{in}~\<open>dir\<close>). These
+ directories should be exclusively assigned to a unique session, without
+ implicit sharing of file-system locations, but
+ \isakeyword{directories}~\<open>dir\<close>~(\isakeyword{overlapping}) is tolerant in
+ this respect (it might cause problems in the Prover IDE @{cite
+ "isabelle-jedit"} to assign session-qualified theory names to open files).
+
\<^descr> \isakeyword{options}~\<open>[x = a, y = b, z]\<close> defines separate options
(\secref{sec:system-options}) that are used when processing this session,
but \<^emph>\<open>without\<close> propagation to child sessions. Note that \<open>z\<close> abbreviates \<open>z =