src/Pure/Isar/keyword.scala
changeset 65385 23f36ab9042b
parent 65384 36255c43c64c
child 66919 1f93e376aeb6
equal deleted inserted replaced
65384:36255c43c64c 65385:23f36ab9042b
    98     val none: Spec = Spec("")
    98     val none: Spec = Spec("")
    99   }
    99   }
   100   sealed case class Spec(kind: String, exts: List[String] = Nil, tags: List[String] = Nil)
   100   sealed case class Spec(kind: String, exts: List[String] = Nil, tags: List[String] = Nil)
   101   {
   101   {
   102     def is_none: Boolean = kind == ""
   102     def is_none: Boolean = kind == ""
       
   103 
       
   104     override def toString: String =
       
   105       kind +
       
   106         (if (exts.isEmpty) "" else " (" + commas_quote(exts) + ")") +
       
   107         (if (tags.isEmpty) "" else tags.map(quote).mkString(" % ", " % ", ""))
   103   }
   108   }
   104 
   109 
   105   object Keywords
   110   object Keywords
   106   {
   111   {
   107     def empty: Keywords = new Keywords()
   112     def empty: Keywords = new Keywords()