changeset 63450 | afd657fffdf9 |
parent 62812 | ce22e5c3d4ce |
child 64370 | 865b39487b5d |
--- 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 = ")]}»›⟩⌉⌋⦈⟧⦄" }