# HG changeset patch # User wenzelm # Date 1429393410 -7200 # Node ID a90982bbe8b43c192a293ca738459b916679e389 # Parent 9cfc45235c2739d6b8e4504ce96ed38eaa4a6728 clarified keywords for quasi-command spans and Sidekick structure; diff -r 9cfc45235c27 -r a90982bbe8b4 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Sat Apr 18 21:13:05 2015 +0200 +++ b/src/Pure/Isar/token.scala Sat Apr 18 23:43:30 2015 +0200 @@ -259,8 +259,9 @@ def is_begin: Boolean = is_keyword && source == "begin" def is_end: Boolean = is_command && source == "end" + // FIXME avoid hard-wired stuff def is_command_modifier: Boolean = - is_keyword && (source == "private" || source == "qualified") + is_keyword && (source == "public" || source == "private" || source == "qualified") def is_begin_block: Boolean = is_command && source == "{" def is_end_block: Boolean = is_command && source == "}" @@ -273,4 +274,3 @@ else if (kind == Token.Kind.COMMENT) Scan.Parsers.comment_content(source) else source } - diff -r 9cfc45235c27 -r a90982bbe8b4 src/Pure/System/options.scala --- a/src/Pure/System/options.scala Sat Apr 18 21:13:05 2015 +0200 +++ b/src/Pure/System/options.scala Sat Apr 18 23:43:30 2015 +0200 @@ -76,7 +76,7 @@ lazy val options_syntax = Outer_Syntax.init() + ":" + "=" + "--" + - (SECTION, Keyword.DOCUMENT_HEADING) + (PUBLIC, Keyword.THY_DECL) + (OPTION, Keyword.THY_DECL) + (SECTION, Keyword.DOCUMENT_HEADING) + PUBLIC + (OPTION, Keyword.THY_DECL) lazy val prefs_syntax = Outer_Syntax.init() + "=" @@ -93,7 +93,7 @@ { command(SECTION) ~! text ^^ { case _ ~ a => (options: Options) => options.set_section(a) } | - opt(command(PUBLIC)) ~ command(OPTION) ~! (position(option_name) ~ $$$(":") ~ option_type ~ + opt($$$(PUBLIC)) ~ command(OPTION) ~! (position(option_name) ~ $$$(":") ~ option_type ~ $$$("=") ~ option_value ~ ($$$("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^ { case a ~ _ ~ ((b, pos) ~ _ ~ c ~ _ ~ d ~ e) => (options: Options) => options.declare(a.isDefined, pos, b, c, d, e) }