# HG changeset patch
# User wenzelm
# Date 1509535913 -3600
# Node ID 43b2aac6053c65f71144300c834f8bf63c52f333
# Parent  13857f49d215ee900ebe56268bb495d8e08b79c5
tuned diagram;

diff -r 13857f49d215 -r 43b2aac6053c src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Wed Nov 01 12:28:20 2017 +0100
+++ b/src/Doc/System/Sessions.thy	Wed Nov 01 12:31:53 2017 +0100
@@ -52,12 +52,9 @@
     @{syntax_def session_chapter}: @'chapter' @{syntax name}
     ;
 
-    @{syntax_def session_entry}: @'session' spec '='
-      (@{syntax system_name} '+')? body
-    ;
-    body: description? options? (sessions?) (theories*) \<newline> (document_files*)
-    ;
-    spec: @{syntax system_name} groups? dir?
+    @{syntax_def session_entry}: @'session' @{syntax system_name} groups? dir? '=' \<newline>
+      (@{syntax system_name} '+')? description? options? \<newline>
+      (sessions?) (theories*) (document_files*)
     ;
     groups: '(' (@{syntax name} +) ')'
     ;