src/Doc/System/Sessions.thy

   \<^rail>\<open>
     @{syntax_def session_chapter}: @'chapter' @{syntax name}
     ;
 
     @{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} +) ')'
     ;
     dir: @'in' @{syntax embedded}
     ;
     description: @'description' @{syntax text}
     ;
+    options: @'options' opts
+    ;
+    opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']'
+    ;
+    value: @{syntax name} | @{syntax real}
+    ;
+    sessions: @'sessions' (@{syntax system_name}+)
+    ;
     directories: @'directories' ((dir ('(' @'overlapping' ')')?) +)
-    ;
-    options: @'options' opts
-    ;
-    opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']'
-    ;
-    value: @{syntax name} | @{syntax real}
-    ;
-    sessions: @'sessions' (@{syntax system_name}+)
     ;
     theories: @'theories' opts? (theory_entry+)
     ;
     theory_entry: @{syntax system_name} ('(' @'global' ')')?
     ;

   All theory files are located relatively to the session directory. The prover
   process is run within the same as its current working directory.
 
   \<^descr> \isakeyword{description}~\<open>text\<close> is a free-form annotation for this
   session.
+
+  \<^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 =
+  true\<close> for Boolean options.
+
+  \<^descr> \isakeyword{sessions}~\<open>names\<close> specifies sessions that are \<^emph>\<open>imported\<close> into
+  the current name space of theories. This allows to refer to a theory \<open>A\<close>
+  from session \<open>B\<close> by the qualified name \<open>B.A\<close> --- although it is loaded again
+  into the current ML process, which is in contrast to a theory that is
+  already present in the \<^emph>\<open>parent\<close> session.
+
+  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{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 =
-  true\<close> for Boolean options.
-
-  \<^descr> \isakeyword{sessions}~\<open>names\<close> specifies sessions that are \<^emph>\<open>imported\<close> into
-  the current name space of theories. This allows to refer to a theory \<open>A\<close>
-  from session \<open>B\<close> by the qualified name \<open>B.A\<close> --- although it is loaded again
-  into the current ML process, which is in contrast to a theory that is
-  already present in the \<^emph>\<open>parent\<close> session.
-
-  Theories that are imported from other sessions are excluded from the current
-  session document.
 
   \<^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
   of \isakeyword{theories} may be given. Options are only active for each