src/Pure/Admin/component_jedit.scala
changeset 82122 f67fb2339eeb
parent 82121 fdaa32d96393
child 82179 bff32e50fe14
--- a/src/Pure/Admin/component_jedit.scala	Sun Feb 09 12:47:21 2025 +0100
+++ b/src/Pure/Admin/component_jedit.scala	Sun Feb 09 12:58:40 2025 +0100
@@ -21,8 +21,8 @@
     val init: Mode =
       empty +
         ("noWordSep" -> Symbol.decode("""_'?\<^sub>\^<>""")) +
-        ("unalignedOpenBrackets" -> "{[(«‹⟨⌈⌊⦇⟦⦃⦉") +
-        ("unalignedCloseBrackets" -> "⦊⦄⟧⦈⌋⌉⟩›»)]}") +
+        ("unalignedOpenBrackets" -> Symbol.open_brackets_decoded) +
+        ("unalignedCloseBrackets" -> Symbol.close_brackets_decoded) +
         ("tabSize" -> "2") +
         ("indentSize" -> "2")