# 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 = """([{\<guillemotleft>\<open>\<langle>\<lceil>\<lfloor>\<lparr>\<lbrakk>\<lbrace>\<llangle>"""
+  val close_brackets = """)]}\<guillemotright>\<close>\<rangle>\<rceil>\<rfloor>\<rparr>\<rbrakk>\<rbrace>\<rrangle>"""
+
+  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")