more uniform header_keywords in ML/Scala;
tuned signature;

--- a/src/Pure/Isar/keyword.scala	Wed Nov 05 21:21:15 2014 +0100
+++ b/src/Pure/Isar/keyword.scala	Wed Nov 05 21:59:21 2014 +0100
@@ -72,8 +72,6 @@
   object Keywords
   {
     def empty: Keywords = new Keywords()
-
-    def apply(keywords: List[String]): Keywords = (empty /: keywords)(_ + _)
   }
 
   class Keywords private(
@@ -99,9 +97,8 @@
 
     /* add keywords */
 
-    def + (name: String): Keywords =
-      new Keywords(minor + name, major, commands)
-
+    def + (name: String): Keywords = new Keywords(minor + name, major, commands)
+    def + (name: String, kind: String): Keywords = this + (name, (kind, Nil))
     def + (name: String, kind: (String, List[String])): Keywords =
     {
       val major1 = major + name

--- a/src/Pure/Isar/outer_syntax.scala	Wed Nov 05 21:21:15 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Wed Nov 05 21:59:21 2014 +0100
@@ -86,6 +86,8 @@
 
   /* add keywords */
 
+  def + (name: String): Outer_Syntax = this + (name, None, None)
+  def + (name: String, kind: String): Outer_Syntax = this + (name, Some((kind, Nil)), None)
   def + (name: String, opt_kind: Option[(String, List[String])], replace: Option[String])
     : Outer_Syntax =
   {
@@ -99,8 +101,6 @@
       else completion + (name, replace getOrElse name)
     new Outer_Syntax(keywords1, completion1, language_context, true)
   }
-  def + (name: String): Outer_Syntax = this + (name, None, None)
-  def + (name: String, kind: String): Outer_Syntax = this + (name, Some((kind, Nil)), None)
 
   def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
     (this /: keywords) {

--- a/src/Pure/Thy/thy_header.ML	Wed Nov 05 21:21:15 2014 +0100
+++ b/src/Pure/Thy/thy_header.ML	Wed Nov 05 21:59:21 2014 +0100
@@ -81,9 +81,13 @@
   Keyword.empty_keywords
   |> fold (Keyword.add o rpair NONE)
     ["%", "(", ")", ",", "::", "==", "and", beginN, importsN, keywordsN]
-  |> fold (Keyword.add o rpair (SOME Keyword.heading))
-    [headerN, chapterN, sectionN, subsectionN, subsubsectionN]
-  |> Keyword.add (theoryN, SOME Keyword.thy_begin);
+  |> fold Keyword.add
+    [(headerN, SOME Keyword.heading),
+     (chapterN, SOME Keyword.heading),
+     (sectionN, SOME Keyword.heading),
+     (subsectionN, SOME Keyword.heading),
+     (subsubsectionN, SOME Keyword.heading),
+     (theoryN, SOME Keyword.thy_begin)];
 
 
 (* header args *)

--- a/src/Pure/Thy/thy_header.scala	Wed Nov 05 21:21:15 2014 +0100
+++ b/src/Pure/Thy/thy_header.scala	Wed Nov 05 21:59:21 2014 +0100
@@ -28,9 +28,14 @@
   val BEGIN = "begin"
 
   private val header_keywords =
-    Keyword.Keywords(
-      List("%", "(", ")", ",", "::", "==", AND, BEGIN,
-        HEADER, CHAPTER, SECTION, SUBSECTION, SUBSUBSECTION, IMPORTS, KEYWORDS, THEORY))
+    Keyword.Keywords.empty +
+      "%" + "(" + ")" + "," + "::" + "==" + AND + BEGIN + IMPORTS + KEYWORDS +
+      (HEADER, Keyword.HEADING) +
+      (CHAPTER, Keyword.HEADING) +
+      (SECTION, Keyword.HEADING) +
+      (SUBSECTION, Keyword.HEADING) +
+      (SUBSUBSECTION, Keyword.HEADING) +
+      (THEORY, Keyword.THY_BEGIN)
 
 
   /* theory file name */
@@ -81,14 +86,14 @@
       { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
 
     val heading =
-      (keyword(HEADER) |
-        keyword(CHAPTER) |
-        keyword(SECTION) |
-        keyword(SUBSECTION) |
-        keyword(SUBSUBSECTION)) ~
+      (command(HEADER) |
+        command(CHAPTER) |
+        command(SECTION) |
+        command(SUBSECTION) |
+        command(SUBSUBSECTION)) ~
       tags ~! document_source
 
-    (rep(heading) ~ keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
+    (rep(heading) ~ command(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
   }