# HG changeset patch
# User wenzelm
# Date 1739633856 -3600
# Node ID 434e6e669b3a3ae3b4dc5534ea0f7bb154c3f16e
# Parent  a519b9d1e1c1758e3573da02e41da2d235a997ff
more complete brackets, as in Isabelle/jEdit;

diff -r a519b9d1e1c1 -r 434e6e669b3a src/Tools/VSCode/extension/isabelle-language.json
--- a/src/Tools/VSCode/extension/isabelle-language.json	Sat Feb 15 16:12:29 2025 +0100
+++ b/src/Tools/VSCode/extension/isabelle-language.json	Sat Feb 15 16:37:36 2025 +0100
@@ -13,7 +13,9 @@
     ["⌊", "⌋"],
     ["⦇", "⦈"],
     ["⟦", "⟧"],
-    ["⦃", "⦄"]
+    ["⦃", "⦄"],
+    ["⟪", "⟫"],
+    ["⦉", "⦊"]
   ],
   "autoClosingPairs": [
     { "open": "(", "close": ")" },
@@ -27,6 +29,8 @@
     { "open": "⦇", "close": "⦈" },
     { "open": "⟦", "close": "⟧" },
     { "open": "⦃", "close": "⦄" },
+    { "open": "⟪", "close": "⟫" },
+    { "open": "⦉", "close": "⦊" },
     { "open": "`", "close": "`", "notIn": ["string"] },
     { "open": "\"", "close": "\"", "notIn": ["string"] }
   ],
@@ -42,6 +46,8 @@
     ["⦇", "⦈"],
     ["⟦", "⟧"],
     ["⦃", "⦄"],
+    ["⟪", "⟫"],
+    ["⦉", "⦊"],
     ["`", "`"],
     ["\"", "\""]
   ],