changeset 58999 | ed09ae4ea2d8 |
parent 58908 | 58bedbc18915 |
child 59083 | 88b0b1f28adc |
--- a/src/Pure/System/options.scala Thu Nov 13 17:28:11 2014 +0100 +++ b/src/Pure/System/options.scala Thu Nov 13 23:45:15 2014 +0100 @@ -76,7 +76,7 @@ lazy val options_syntax = Outer_Syntax.init() + ":" + "=" + "--" + - (SECTION, Keyword.HEADING) + (PUBLIC, Keyword.THY_DECL) + (OPTION, Keyword.THY_DECL) + (SECTION, Keyword.DOCUMENT_HEADING) + (PUBLIC, Keyword.THY_DECL) + (OPTION, Keyword.THY_DECL) lazy val prefs_syntax = Outer_Syntax.init() + "="