# HG changeset patch
# User wenzelm
# Date 1415214332 -3600
# Node ID 938bbacda12d13dac3a59d8b30533061a02d5177
# Parent  47809a811ebae6f2dfae146c9866beb12ce93c5e
tuned;

diff -r 47809a811eba -r 938bbacda12d src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Wed Nov 05 17:37:25 2014 +0100
+++ b/src/Pure/Isar/keyword.scala	Wed Nov 05 20:05:32 2014 +0100
@@ -85,16 +85,6 @@
 
     def is_empty: Boolean = minor.isEmpty && major.isEmpty
 
-    def + (name: String): Keywords =
-      new Keywords(minor + name, major, command_kinds)
-
-    def + (name: String, kind: (String, List[String])): Keywords =
-    {
-      val major1 = major + name
-      val command_kinds1 = command_kinds + (name -> kind)
-      new Keywords(minor, major1, command_kinds1)
-    }
-
     override def toString: String =
     {
       val keywords = minor.iterator.map(quote(_)).toList
@@ -107,6 +97,19 @@
     }
 
 
+    /* add keywords */
+
+    def + (name: String): Keywords =
+      new Keywords(minor + name, major, command_kinds)
+
+    def + (name: String, kind: (String, List[String])): Keywords =
+    {
+      val major1 = major + name
+      val command_kinds1 = command_kinds + (name -> kind)
+      new Keywords(minor, major1, command_kinds1)
+    }
+
+
     /* command kind */
 
     def command_kind(name: String): Option[String] = command_kinds.get(name).map(_._1)