# HG changeset patch
# User wenzelm
# Date 1345799032 -7200
# Node ID f45ccc0d1ace457e96583ae3665f785d0b1407be
# Parent  34fac6fb9b032b91e93f66b3d5b8001a4e58d4fc
clarified syntax boundary cases and errors;

diff -r 34fac6fb9b03 -r f45ccc0d1ace doc-src/System/Thy/Sessions.thy
--- a/doc-src/System/Thy/Sessions.thy	Thu Aug 23 21:23:14 2012 +0200
+++ b/doc-src/System/Thy/Sessions.thy	Fri Aug 24 11:03:52 2012 +0200
@@ -48,7 +48,7 @@
   @{rail "
     @{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body
     ;
-    body: description? options? ( theories * ) files?
+    body: description? options? ( theories + ) files?
     ;
     spec: @{syntax name} groups? dir?
     ;
diff -r 34fac6fb9b03 -r f45ccc0d1ace doc-src/System/Thy/document/Sessions.tex
--- a/doc-src/System/Thy/document/Sessions.tex	Thu Aug 23 21:23:14 2012 +0200
+++ b/doc-src/System/Thy/document/Sessions.tex	Fri Aug 24 11:03:52 2012 +0200
@@ -90,8 +90,8 @@
 \rail@nont{\isa{options}}[]
 \rail@endbar
 \rail@plus
+\rail@nont{\isa{theories}}[]
 \rail@nextplus{1}
-\rail@cnont{\isa{theories}}[]
 \rail@endplus
 \rail@bar
 \rail@nextbar{1}
diff -r 34fac6fb9b03 -r f45ccc0d1ace src/Pure/ROOT
--- a/src/Pure/ROOT	Thu Aug 23 21:23:14 2012 +0200
+++ b/src/Pure/ROOT	Fri Aug 24 11:03:52 2012 +0200
@@ -1,4 +1,5 @@
 session RAW =
+  theories
   files
     "General/exn.ML"
     "ML-Systems/compiler_polyml.ML"
diff -r 34fac6fb9b03 -r f45ccc0d1ace src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Thu Aug 23 21:23:14 2012 +0200
+++ b/src/Pure/System/build.scala	Fri Aug 24 11:03:52 2012 +0200
@@ -185,7 +185,7 @@
             (opt(session_name ~! keyword("+") ^^ { case x ~ _ => x }) ~
               ((keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
               ((keyword(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
-              rep(theories) ~
+              rep1(theories) ~
               ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil))))) ^^
         { case _ ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h))) =>
             Session_Entry(pos, a, b, c, d, e, f, g, h) }