src/Pure/System/options.scala
changeset 59811 6b0d9e8ac227
parent 59705 740a0ca7e09b
child 60133 a90982bbe8b4
equal deleted inserted replaced
59810:e749a0f2f401 59811:6b0d9e8ac227
    91 
    91 
    92     val option_entry: Parser[Options => Options] =
    92     val option_entry: Parser[Options => Options] =
    93     {
    93     {
    94       command(SECTION) ~! text ^^
    94       command(SECTION) ~! text ^^
    95         { case _ ~ a => (options: Options) => options.set_section(a) } |
    95         { case _ ~ a => (options: Options) => options.set_section(a) } |
    96       opt(command(PUBLIC)) ~ position(command(OPTION)) ~! (option_name ~ $$$(":") ~ option_type ~
    96       opt(command(PUBLIC)) ~ command(OPTION) ~! (position(option_name) ~ $$$(":") ~ option_type ~
    97       $$$("=") ~ option_value ~ ($$$("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
    97       $$$("=") ~ option_value ~ ($$$("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
    98         { case a ~ ((_, pos)) ~ (b ~ _ ~ c ~ _ ~ d ~ e) =>
    98         { case a ~ _ ~ ((b, pos) ~ _ ~ c ~ _ ~ d ~ e) =>
    99             (options: Options) => options.declare(a.isDefined, pos, b, c, d, e) }
    99             (options: Options) => options.declare(a.isDefined, pos, b, c, d, e) }
   100     }
   100     }
   101 
   101 
   102     val prefs_entry: Parser[Options => Options] =
   102     val prefs_entry: Parser[Options => Options] =
   103     {
   103     {