src/Pure/General/word.scala

   def explode(sep: Char, text: String): List[String] =
     explode(_ == sep, text)
 
   def explode(text: String): List[String] =
     explode(Character.isWhitespace(_), text)
+
+
+  /* brackets */
+
+  val open_brackets = "([{«‹⟨⌈⌊⦇⟦⦃"
+  val close_brackets = ")]}»›⟩⌉⌋⦈⟧⦄"
 }