author | wenzelm |
Tue, 04 Apr 2017 23:12:08 +0200 | |
changeset 65385 | 23f36ab9042b |
parent 65384 | 36255c43c64c |
child 65386 | e3fb3036a00e |
--- a/src/Pure/Isar/keyword.scala Tue Apr 04 22:56:28 2017 +0200 +++ b/src/Pure/Isar/keyword.scala Tue Apr 04 23:12:08 2017 +0200 @@ -100,6 +100,11 @@ sealed case class Spec(kind: String, exts: List[String] = Nil, tags: List[String] = Nil) { def is_none: Boolean = kind == "" + + override def toString: String = + kind + + (if (exts.isEmpty) "" else " (" + commas_quote(exts) + ")") + + (if (tags.isEmpty) "" else tags.map(quote).mkString(" % ", " % ", "")) } object Keywords