--- a/src/Pure/System/options.scala Tue Aug 07 19:16:58 2012 +0200
+++ b/src/Pure/System/options.scala Tue Aug 07 20:28:35 2012 +0200
@@ -30,13 +30,13 @@
/* parsing */
+ private val DECLARE = "declare"
+ private val DEFINE = "define"
+
+ lazy val options_syntax = Outer_Syntax.init() + ":" + "=" + "--" + DECLARE + DEFINE
+
private object Parser extends Parse.Parser
{
- val DECLARE = "declare"
- val DEFINE = "define"
-
- val syntax = Outer_Syntax.empty + ":" + "=" + "--" + DECLARE + DEFINE
-
val entry: Parser[Options => Options] =
{
val option_name = atom("option name", _.is_xname)
@@ -56,7 +56,8 @@
def parse_entries(file: Path): List[Options => Options] =
{
- parse_all(rep(entry), Token.reader(syntax.scan(File.read(file)), file.implode)) match {
+ val toks = options_syntax.scan(File.read(file))
+ parse_all(rep(entry), Token.reader(toks, file.implode)) match {
case Success(result, _) => result
case bad => error(bad.toString)
}