equal
deleted
inserted
replaced
50 |
50 |
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' spec '=' (@{syntax name} '+')? body |
55 @{syntax_def session_entry}: @'session' spec '=' |
|
56 (@{syntax system_name} '+')? body |
56 ; |
57 ; |
57 body: description? options? (theories+) \<newline> (document_files*) |
58 body: description? options? (theories+) \<newline> (document_files*) |
58 ; |
59 ; |
59 spec: @{syntax name} groups? dir? |
60 spec: @{syntax system_name} groups? dir? |
60 ; |
61 ; |
61 groups: '(' (@{syntax name} +) ')' |
62 groups: '(' (@{syntax name} +) ')' |
62 ; |
63 ; |
63 dir: @'in' @{syntax name} |
64 dir: @'in' @{syntax name} |
64 ; |
65 ; |
68 ; |
69 ; |
69 opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']' |
70 opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']' |
70 ; |
71 ; |
71 value: @{syntax name} | @{syntax real} |
72 value: @{syntax name} | @{syntax real} |
72 ; |
73 ; |
73 sessions: @'sessions' (@{syntax name}+) |
74 sessions: @'sessions' (@{syntax system_name}+) |
74 ; |
75 ; |
75 theories: @'theories' opts? (theory_entry*) |
76 theories: @'theories' opts? (theory_entry*) |
76 ; |
77 ; |
77 theory_entry: @{syntax name} ('(' @'global' ')')? |
78 theory_entry: @{syntax system_name} ('(' @'global' ')')? |
78 ; |
79 ; |
79 document_files: @'document_files' ('(' dir ')')? (@{syntax name}+) |
80 document_files: @'document_files' ('(' dir ')')? (@{syntax name}+) |
80 \<close>} |
81 \<close>} |
81 |
82 |
82 \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on |
83 \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on |