diff -r 56d70f7ce4a4 -r 36c8c32346cb src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sun Sep 08 17:15:46 2019 +0200
+++ b/src/Doc/System/Sessions.thy	Sun Sep 08 17:49:35 2019 +0200
@@ -53,9 +53,9 @@
     ;
 
     @{syntax_def session_entry}: @'session' @{syntax system_name} groups? dir? '=' \<newline>
-      (@{syntax system_name} '+')? description? directories?  \<newline>
-      options? (sessions?) (theories*) (document_files*) \<newline>
-      (export_files*)
+      (@{syntax system_name} '+')? description? options? \<newline>
+      sessions? directories? (theories*) \<newline>
+      (document_files*) (export_files*)
     ;
     groups: '(' (@{syntax name} +) ')'
     ;
@@ -63,8 +63,6 @@
     ;
     description: @'description' @{syntax text}
     ;
-    directories: @'directories' ((dir ('(' @'overlapping' ')')?) +)
-    ;
     options: @'options' opts
     ;
     opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']'
@@ -73,6 +71,8 @@
     ;
     sessions: @'sessions' (@{syntax system_name}+)
     ;
+    directories: @'directories' ((dir ('(' @'overlapping' ')')?) +)
+    ;
     theories: @'theories' opts? (theory_entry+)
     ;
     theory_entry: @{syntax system_name} ('(' @'global' ')')?
@@ -110,16 +110,6 @@
   \<^descr> \isakeyword{description}~\<open>text\<close> is a free-form annotation for this
   session.
 
-  \<^descr> \isakeyword{directories}~\<open>dirs\<close> specifies additional directories for
-  import of theory files via \isakeyword{theories} within \<^verbatim>\<open>ROOT\<close> or
-  \<^theory_text>\<open>imports\<close> within a theory; \<open>dirs\<close> are relative to the main session
-  directory (cf.\ \isakeyword{session} \dots \isakeyword{in}~\<open>dir\<close>). These
-  directories should be exclusively assigned to a unique session, without
-  implicit sharing of file-system locations, but
-  \isakeyword{directories}~\<open>dir\<close>~(\isakeyword{overlapping}) is tolerant in
-  this respect (it might cause problems in the Prover IDE @{cite
-  "isabelle-jedit"} to assign session-qualified theory names to open files).
-
   \<^descr> \isakeyword{options}~\<open>[x = a, y = b, z]\<close> defines separate options
   (\secref{sec:system-options}) that are used when processing this session,
   but \<^emph>\<open>without\<close> propagation to child sessions. Note that \<open>z\<close> abbreviates \<open>z =
@@ -134,6 +124,16 @@
   Theories that are imported from other sessions are excluded from the current
   session document.
 
+  \<^descr> \isakeyword{directories}~\<open>dirs\<close> specifies additional directories for
+  import of theory files via \isakeyword{theories} within \<^verbatim>\<open>ROOT\<close> or
+  \<^theory_text>\<open>imports\<close> within a theory; \<open>dirs\<close> are relative to the main session
+  directory (cf.\ \isakeyword{session} \dots \isakeyword{in}~\<open>dir\<close>). These
+  directories should be exclusively assigned to a unique session, without
+  implicit sharing of file-system locations, but
+  \isakeyword{directories}~\<open>dir\<close>~(\isakeyword{overlapping}) is tolerant in
+  this respect (it might cause problems in the Prover IDE @{cite
+  "isabelle-jedit"} to assign session-qualified theory names to open files).
+
   \<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a block of theories that
   are processed within an environment that is augmented by the given options,
   in addition to the global session options given before. Any number of blocks