51 \<^rail>\<open> |
51 \<^rail>\<open> |
52 @{syntax_def session_chapter}: @'chapter' @{syntax name} |
52 @{syntax_def session_chapter}: @'chapter' @{syntax name} |
53 ; |
53 ; |
54 |
54 |
55 @{syntax_def session_entry}: @'session' @{syntax system_name} groups? dir? '=' \<newline> |
55 @{syntax_def session_entry}: @'session' @{syntax system_name} groups? dir? '=' \<newline> |
56 (@{syntax system_name} '+')? description? options? \<newline> |
56 (@{syntax system_name} '+')? description? directories? \<newline> |
57 (sessions?) (theories*) (document_files*) \<newline> (export_files*) |
57 options? (sessions?) (theories*) (document_files*) \<newline> |
|
58 (export_files*) |
58 ; |
59 ; |
59 groups: '(' (@{syntax name} +) ')' |
60 groups: '(' (@{syntax name} +) ')' |
60 ; |
61 ; |
61 dir: @'in' @{syntax embedded} |
62 dir: @'in' @{syntax embedded} |
62 ; |
63 ; |
63 description: @'description' @{syntax text} |
64 description: @'description' @{syntax text} |
|
65 ; |
|
66 directories: @'directories' ((dir ('(' @'overlapping' ')')?) +) |
64 ; |
67 ; |
65 options: @'options' opts |
68 options: @'options' opts |
66 ; |
69 ; |
67 opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']' |
70 opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']' |
68 ; |
71 ; |
104 All theory files are located relatively to the session directory. The prover |
107 All theory files are located relatively to the session directory. The prover |
105 process is run within the same as its current working directory. |
108 process is run within the same as its current working directory. |
106 |
109 |
107 \<^descr> \isakeyword{description}~\<open>text\<close> is a free-form annotation for this |
110 \<^descr> \isakeyword{description}~\<open>text\<close> is a free-form annotation for this |
108 session. |
111 session. |
|
112 |
|
113 \<^descr> \isakeyword{directories}~\<open>dirs\<close> specifies additional directories for |
|
114 import of theory files via \isakeyword{theories} within \<^verbatim>\<open>ROOT\<close> or |
|
115 \<^theory_text>\<open>imports\<close> within a theory; \<open>dirs\<close> are relative to the main session |
|
116 directory (cf.\ \isakeyword{session} \dots \isakeyword{in}~\<open>dir\<close>). These |
|
117 directories should be exclusively assigned to a unique session, without |
|
118 implicit sharing of file-system locations, but |
|
119 \isakeyword{directories}~\<open>dir\<close>~(\isakeyword{overlapping}) is tolerant in |
|
120 this respect (it might cause problems in the Prover IDE @{cite |
|
121 "isabelle-jedit"} to assign session-qualified theory names to open files). |
109 |
122 |
110 \<^descr> \isakeyword{options}~\<open>[x = a, y = b, z]\<close> defines separate options |
123 \<^descr> \isakeyword{options}~\<open>[x = a, y = b, z]\<close> defines separate options |
111 (\secref{sec:system-options}) that are used when processing this session, |
124 (\secref{sec:system-options}) that are used when processing this session, |
112 but \<^emph>\<open>without\<close> propagation to child sessions. Note that \<open>z\<close> abbreviates \<open>z = |
125 but \<^emph>\<open>without\<close> propagation to child sessions. Note that \<open>z\<close> abbreviates \<open>z = |
113 true\<close> for Boolean options. |
126 true\<close> for Boolean options. |