src/Pure/System/options.scala

       atom("option value", tok => tok.is_name || tok.is_float)
 
     val option_entry: Parser[Options => Options] =
     {
       command(SECTION) ~! text ^^
-        { case _ ~ a => (options: Options) => options.set_section(a.trim) } |
+        { case _ ~ a => (options: Options) => options.set_section(a) } |
       command(OPTION) ~! (option_name ~ keyword(":") ~ option_type ~
       keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
         { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) => (options: Options) => options.declare(a, b, c, d) }
     }