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 '=' |
55 @{syntax_def session_entry}: @'session' @{syntax system_name} groups? dir? '=' \<newline> |
56 (@{syntax system_name} '+')? body |
56 (@{syntax system_name} '+')? description? options? \<newline> |
57 ; |
57 (sessions?) (theories*) (document_files*) |
58 body: description? options? (sessions?) (theories*) \<newline> (document_files*) |
|
59 ; |
|
60 spec: @{syntax system_name} groups? dir? |
|
61 ; |
58 ; |
62 groups: '(' (@{syntax name} +) ')' |
59 groups: '(' (@{syntax name} +) ')' |
63 ; |
60 ; |
64 dir: @'in' @{syntax name} |
61 dir: @'in' @{syntax name} |
65 ; |
62 ; |