changeset 82120 | a4aa45999dd7 |
parent 81647 | ae670d860912 |
child 82124 | 1eda03781f76 |
--- a/src/Pure/General/word.scala Sun Feb 09 12:14:09 2025 +0100 +++ b/src/Pure/General/word.scala Sun Feb 09 12:35:29 2025 +0100 @@ -77,10 +77,4 @@ explode(Character.isWhitespace _, text) def informal(text: String): String = implode(explode('_', text)) - - - /* brackets */ - - val open_brackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪" - val close_brackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫" }