src/Pure/General/word.scala

--- a/src/Pure/General/word.scala	Mon Jul 11 19:03:08 2016 +0200
+++ b/src/Pure/General/word.scala	Mon Jul 11 20:37:28 2016 +0200
@@ -96,4 +96,10 @@
 
   def explode(text: String): List[String] =
     explode(Character.isWhitespace(_), text)
+
+
+  /* brackets */
+
+  val open_brackets = "([{«‹⟨⌈⌊⦇⟦⦃"
+  val close_brackets = ")]}»›⟩⌉⌋⦈⟧⦄"
 }