# HG changeset patch # User wenzelm # Date 1567955746 -7200 # Node ID 56d70f7ce4a4432fbf1e7a65370111d19a709fae # Parent 73812c598a269b138b9a640420514e4c726e3d81 more documentation; diff -r 73812c598a26 -r 56d70f7ce4a4 NEWS --- 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 diff -r 73812c598a26 -r 56d70f7ce4a4 src/Doc/System/Sessions.thy --- 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? '=' \ - (@{syntax system_name} '+')? description? options? \ - (sessions?) (theories*) (document_files*) \ (export_files*) + (@{syntax system_name} '+')? description? directories? \ + options? (sessions?) (theories*) (document_files*) \ + (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}~\text\ is a free-form annotation for this session. + \<^descr> \isakeyword{directories}~\dirs\ specifies additional directories for + import of theory files via \isakeyword{theories} within \<^verbatim>\ROOT\ or + \<^theory_text>\imports\ within a theory; \dirs\ are relative to the main session + directory (cf.\ \isakeyword{session} \dots \isakeyword{in}~\dir\). These + directories should be exclusively assigned to a unique session, without + implicit sharing of file-system locations, but + \isakeyword{directories}~\dir\~(\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}~\[x = a, y = b, z]\ defines separate options (\secref{sec:system-options}) that are used when processing this session, but \<^emph>\without\ propagation to child sessions. Note that \z\ abbreviates \z =