print like syntax of Thy_Header.header;
authorwenzelm
Tue Apr 04 23:12:08 2017 +0200 (2017-04-04)
changeset 6538523f36ab9042b
parent 65384 36255c43c64c
child 65386 e3fb3036a00e
print like syntax of Thy_Header.header;
src/Pure/Isar/keyword.scala
     1.1 --- a/src/Pure/Isar/keyword.scala	Tue Apr 04 22:56:28 2017 +0200
     1.2 +++ b/src/Pure/Isar/keyword.scala	Tue Apr 04 23:12:08 2017 +0200
     1.3 @@ -100,6 +100,11 @@
     1.4    sealed case class Spec(kind: String, exts: List[String] = Nil, tags: List[String] = Nil)
     1.5    {
     1.6      def is_none: Boolean = kind == ""
     1.7 +
     1.8 +    override def toString: String =
     1.9 +      kind +
    1.10 +        (if (exts.isEmpty) "" else " (" + commas_quote(exts) + ")") +
    1.11 +        (if (tags.isEmpty) "" else tags.map(quote).mkString(" % ", " % ", ""))
    1.12    }
    1.13  
    1.14    object Keywords