tuned;
authorwenzelm
Wed, 05 Nov 2014 20:05:32 +0100
changeset 58902 938bbacda12d
parent 58901 47809a811eba
child 58903 38c72f5f6c2e
tuned;
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)