--- 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?
;
--- 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}
--- 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"
--- 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) }