--- 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
--- 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
--- 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")
--- 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