# 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) }