# HG changeset patch
# User wenzelm
# Date 1491340328 -7200
# Node ID 23f36ab9042b1a1c46bfa1f116901d48f7f901b9
# Parent  36255c43c64cc9d7ab3f22f8e66b8d1bc1fd9828
print like syntax of Thy_Header.header;

diff -r 36255c43c64c -r 23f36ab9042b 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