print like syntax of Thy_Header.header;
authorwenzelm
Tue, 04 Apr 2017 23:12:08 +0200
changeset 65385 23f36ab9042b
parent 65384 36255c43c64c
child 65386 e3fb3036a00e
print like syntax of Thy_Header.header;
src/Pure/Isar/keyword.scala
--- 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