# HG changeset patch
# User wenzelm
# Date 1739102320 -3600
# Node ID f67fb2339eeb9dcb06b6b73912a37fbc7c320547
# Parent  fdaa32d96393bc2a536a505b3c81e3111a50b297
more complete brackets for jEdit modes;
tuned: more robust Isabelle symbols;

diff -r fdaa32d96393 -r f67fb2339eeb Admin/components/components.sha1
--- a/Admin/components/components.sha1	Sun Feb 09 12:47:21 2025 +0100
+++ b/Admin/components/components.sha1	Sun Feb 09 12:58:40 2025 +0100
@@ -259,6 +259,7 @@
 a8b11ddf7f6838ea53868e46cb4555b7fa60e776 jedit-20241115.tar.gz
 6a5d78867dc6f692f8f3ab758e3ac1b86fabd3bf jedit-20250129.tar.gz
 011d322d4ae1f8c57112bd695f5e812e48e1d953 jedit-20250130.tar.gz
+8a1a29b585240766a34784e152f769d0df007425 jedit-20250209.tar.gz
 44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
 a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
 4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
diff -r fdaa32d96393 -r f67fb2339eeb Admin/components/main
--- a/Admin/components/main	Sun Feb 09 12:47:21 2025 +0100
+++ b/Admin/components/main	Sun Feb 09 12:58:40 2025 +0100
@@ -16,7 +16,7 @@
 isabelle_setup-20240327
 javamail-20250122
 jdk-21.0.6
-jedit-20250130
+jedit-20250209
 jfreechart-1.5.3
 jortho-1.0-2
 jsoup-1.18.3
diff -r fdaa32d96393 -r f67fb2339eeb src/Pure/Admin/component_jedit.scala
--- 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")
 
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 = """([{\<guillemotleft>\<open>\<langle>\<lceil>\<lfloor>\<lparr>\<lbrakk>\<lbrace>\<llangle>"""
-  val close_brackets = """)]}\<guillemotright>\<close>\<rangle>\<rceil>\<rfloor>\<rparr>\<rbrakk>\<rbrace>\<rrangle>"""
+  val open_brackets = """([{\<guillemotleft>\<open>\<langle>\<lceil>\<lfloor>\<lparr>\<lbrakk>\<lbrace>\<llangle>\<lblot>"""
+  val close_brackets = """)]}\<guillemotright>\<close>\<rangle>\<rceil>\<rfloor>\<rparr>\<rbrakk>\<rbrace>\<rrangle>\<rblot>"""
 
   def open_brackets_decoded = symbols.open_brackets_decoded
   def close_brackets_decoded = symbols.close_brackets_decoded