69 ; |
69 ; |
70 value: @{syntax name} | @{syntax real} |
70 value: @{syntax name} | @{syntax real} |
71 ; |
71 ; |
72 sessions: @'sessions' (@{syntax system_name}+) |
72 sessions: @'sessions' (@{syntax system_name}+) |
73 ; |
73 ; |
74 directories: @'directories' ((dir ('(' @'overlapping' ')')?) +) |
74 directories: @'directories' (dir+) |
75 ; |
75 ; |
76 theories: @'theories' opts? (theory_entry+) |
76 theories: @'theories' opts? (theory_entry+) |
77 ; |
77 ; |
78 theory_entry: @{syntax system_name} ('(' @'global' ')')? |
78 theory_entry: @{syntax system_name} ('(' @'global' ')')? |
79 ; |
79 ; |
126 |
126 |
127 \<^descr> \isakeyword{directories}~\<open>dirs\<close> specifies additional directories for |
127 \<^descr> \isakeyword{directories}~\<open>dirs\<close> specifies additional directories for |
128 import of theory files via \isakeyword{theories} within \<^verbatim>\<open>ROOT\<close> or |
128 import of theory files via \isakeyword{theories} within \<^verbatim>\<open>ROOT\<close> or |
129 \<^theory_text>\<open>imports\<close> within a theory; \<open>dirs\<close> are relative to the main session |
129 \<^theory_text>\<open>imports\<close> within a theory; \<open>dirs\<close> are relative to the main session |
130 directory (cf.\ \isakeyword{session} \dots \isakeyword{in}~\<open>dir\<close>). These |
130 directory (cf.\ \isakeyword{session} \dots \isakeyword{in}~\<open>dir\<close>). These |
131 directories should be exclusively assigned to a unique session, without |
131 directories need to be exclusively assigned to a unique session, without |
132 implicit sharing of file-system locations, but |
132 implicit sharing of file-system locations. |
133 \isakeyword{directories}~\<open>dir\<close>~(\isakeyword{overlapping}) is tolerant in |
|
134 this respect (it might cause problems in the Prover IDE @{cite |
|
135 "isabelle-jedit"} to assign session-qualified theory names to open files). |
|
136 |
133 |
137 \<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a block of theories that |
134 \<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a block of theories that |
138 are processed within an environment that is augmented by the given options, |
135 are processed within an environment that is augmented by the given options, |
139 in addition to the global session options given before. Any number of blocks |
136 in addition to the global session options given before. Any number of blocks |
140 of \isakeyword{theories} may be given. Options are only active for each |
137 of \isakeyword{theories} may be given. Options are only active for each |