diff -r fdaa32d96393 -r f67fb2339eeb src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Sun Feb 09 12:47:21 2025 +0100 +++ b/src/Pure/General/symbol.scala Sun Feb 09 12:58:40 2025 +0100 @@ -637,8 +637,8 @@ /* brackets */ - val open_brackets = """([{\\\\\\\\\""" - val close_brackets = """)]}\\\\\\\\\""" + val open_brackets = """([{\\\\\\\\\\""" + val close_brackets = """)]}\\\\\\\\\\""" def open_brackets_decoded = symbols.open_brackets_decoded def close_brackets_decoded = symbols.close_brackets_decoded