68 ; |
68 ; |
69 opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']' |
69 opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']' |
70 ; |
70 ; |
71 value: @{syntax name} | @{syntax real} |
71 value: @{syntax name} | @{syntax real} |
72 ; |
72 ; |
73 theories: @'theories' opts? ( @{syntax name} * ) |
73 theory_entry: @{syntax name} ('(' @'global' ')')? |
|
74 ; |
|
75 theories: @'theories' opts? (theory_entry*) |
74 ; |
76 ; |
75 files: @'files' (@{syntax name}+) |
77 files: @'files' (@{syntax name}+) |
76 ; |
78 ; |
77 document_files: @'document_files' ('(' dir ')')? (@{syntax name}+) |
79 document_files: @'document_files' ('(' dir ')')? (@{syntax name}+) |
78 \<close>} |
80 \<close>} |
113 \<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a block of theories that |
115 \<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a block of theories that |
114 are processed within an environment that is augmented by the given options, |
116 are processed within an environment that is augmented by the given options, |
115 in addition to the global session options given before. Any number of blocks |
117 in addition to the global session options given before. Any number of blocks |
116 of \isakeyword{theories} may be given. Options are only active for each |
118 of \isakeyword{theories} may be given. Options are only active for each |
117 \isakeyword{theories} block separately. |
119 \isakeyword{theories} block separately. |
|
120 |
|
121 A theory name that is followed by \<open>(\<close>\isakeyword{global}\<open>)\<close> is treated |
|
122 literally in other session specifications or theory imports. In contrast, |
|
123 the default is to qualify theory names by the session name, in order to |
|
124 ensure globally unique names in big session trees. |
118 |
125 |
119 \<^descr> \isakeyword{files}~\<open>files\<close> lists additional source files that are involved |
126 \<^descr> \isakeyword{files}~\<open>files\<close> lists additional source files that are involved |
120 in the processing of this session. This should cover anything outside the |
127 in the processing of this session. This should cover anything outside the |
121 formal content of the theory sources. In contrast, files that are loaded |
128 formal content of the theory sources. In contrast, files that are loaded |
122 formally within a theory, e.g.\ via @{command "ML_file"}, need not be |
129 formally within a theory, e.g.\ via @{command "ML_file"}, need not be |