# HG changeset patch
# User wenzelm
# Date 1509535700 -3600
# Node ID 13857f49d215ee900ebe56268bb495d8e08b79c5
# Parent  39077839947e63ad89fa690b3deb07b48f523f6a
clarified ROOT syntax: 'sessions' and 'theories' are optional, but need to be non-empty;

diff -r 39077839947e -r 13857f49d215 src/Doc/ROOT
--- a/src/Doc/ROOT	Tue Oct 31 22:17:38 2017 +0100
+++ b/src/Doc/ROOT	Wed Nov 01 12:28:20 2017 +0100
@@ -127,7 +127,6 @@
 
 session Intro (doc) in "Intro" = Pure +
   options [document_variants = "intro"]
-  theories
   document_files (in "..")
     "prepare_document"
     "pdfsetup.sty"
@@ -272,7 +271,6 @@
 
 session Logics (doc) in "Logics" = Pure +
   options [document_variants = "logics"]
-  theories
   document_files (in "..")
     "prepare_document"
     "pdfsetup.sty"
@@ -328,7 +326,6 @@
 
 session Nitpick (doc) in "Nitpick" = Pure +
   options [document_variants = "nitpick"]
-  theories
   document_files (in "..")
     "prepare_document"
     "pdfsetup.sty"
@@ -364,7 +361,6 @@
 
 session Sledgehammer (doc) in "Sledgehammer" = Pure +
   options [document_variants = "sledgehammer"]
-  theories
   document_files (in "..")
     "prepare_document"
     "pdfsetup.sty"
diff -r 39077839947e -r 13857f49d215 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Tue Oct 31 22:17:38 2017 +0100
+++ b/src/Doc/System/Sessions.thy	Wed Nov 01 12:28:20 2017 +0100
@@ -55,7 +55,7 @@
     @{syntax_def session_entry}: @'session' spec '='
       (@{syntax system_name} '+')? body
     ;
-    body: description? options? (theories+) \<newline> (document_files*)
+    body: description? options? (sessions?) (theories*) \<newline> (document_files*)
     ;
     spec: @{syntax system_name} groups? dir?
     ;
@@ -73,7 +73,7 @@
     ;
     sessions: @'sessions' (@{syntax system_name}+)
     ;
-    theories: @'theories' opts? (theory_entry*)
+    theories: @'theories' opts? (theory_entry+)
     ;
     theory_entry: @{syntax system_name} ('(' @'global' ')')?
     ;
diff -r 39077839947e -r 13857f49d215 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Oct 31 22:17:38 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Nov 01 12:28:20 2017 +0100
@@ -691,7 +691,7 @@
 
       val theories =
         $$$(THEORIES) ~!
-          ((options | success(Nil)) ~ rep(theory_entry)) ^^
+          ((options | success(Nil)) ~ rep1(theory_entry)) ^^
           { case _ ~ (x ~ y) => (x, y) }
 
       val document_files =
@@ -708,8 +708,8 @@
             (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
               (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
               (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
-              (($$$(SESSIONS) ~! rep(session_name)  ^^ { case _ ~ x => x }) | success(Nil)) ~
-              rep1(theories) ~
+              (($$$(SESSIONS) ~! rep1(session_name)  ^^ { case _ ~ x => x }) | success(Nil)) ~
+              rep(theories) ~
               (rep(document_files) ^^ (x => x.flatten))))) ^^
         { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
             Session_Entry(pos, a, b, c, d, e, f, g, h, i) }