# HG changeset patch # User wenzelm # Date 1739100929 -3600 # Node ID a4aa45999dd74c6f2f34b99ae3451edbe3797e88 # Parent b7929e1dc4fb6c82a63de1408ab02f9355888458 clarified modules: more robust Isabelle symbols; diff -r b7929e1dc4fb -r a4aa45999dd7 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Sun Feb 09 12:14:09 2025 +0100 +++ b/src/Pure/General/symbol.scala Sun Feb 09 12:35:29 2025 +0100 @@ -525,6 +525,12 @@ val close_decoded: Symbol = decode(close) + /* brackets */ + + val open_brackets_decoded = decode(open_brackets) + val close_brackets_decoded = decode(close_brackets) + + /* control symbols */ val control_decoded: Set[Symbol] = @@ -629,6 +635,15 @@ def is_symbolic_char(sym: Symbol): Boolean = symbols.sym_chars.contains(sym) + /* brackets */ + + val open_brackets = """([{\\\\\\\\\""" + val close_brackets = """)]}\\\\\\\\\""" + + def open_brackets_decoded = symbols.open_brackets_decoded + def close_brackets_decoded = symbols.close_brackets_decoded + + /* control symbols */ val control_prefix = "\\<^" diff -r b7929e1dc4fb -r a4aa45999dd7 src/Pure/General/word.scala --- 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 = ")]}»›⟩⌉⌋⦈⟧⦄⟫" } diff -r b7929e1dc4fb -r a4aa45999dd7 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Sun Feb 09 12:14:09 2025 +0100 +++ b/src/Pure/Isar/token.scala Sun Feb 09 12:35:29 2025 +0100 @@ -295,8 +295,8 @@ source.startsWith(Symbol.open) || source.startsWith(Symbol.open_decoded)) - def is_open_bracket: Boolean = is_keyword && Word.open_brackets.exists(is_keyword) - def is_close_bracket: Boolean = is_keyword && Word.close_brackets.exists(is_keyword) + def is_open_bracket: Boolean = is_keyword && Symbol.open_brackets_decoded.exists(is_keyword) + def is_close_bracket: Boolean = is_keyword && Symbol.close_brackets_decoded.exists(is_keyword) def is_begin: Boolean = is_keyword("begin") def is_end: Boolean = is_command("end")