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