# HG changeset patch
# User wenzelm
# Date 1345462781 -7200
# Node ID 8967b42db2d57a4f27f38ff4deab86e624d76277
# Parent  461be56c312f0c8392b86fca06f2a7516c5c4a94
more strict syntax, according to manual;

diff -r 461be56c312f -r 8967b42db2d5 src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Mon Aug 20 08:40:18 2012 +0200
+++ b/src/Pure/System/build.scala	Mon Aug 20 13:39:41 2012 +0200
@@ -171,7 +171,7 @@
 
       val option =
         name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
-      val options = keyword("[") ~> repsep(option, keyword(",")) <~ keyword("]")
+      val options = keyword("[") ~> rep1sep(option, keyword(",")) <~ keyword("]")
 
       val theories =
         keyword(THEORIES) ~! ((options | success(Nil)) ~ rep(theory_name)) ^^