# 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 @@ ["⦇", "⦈"], ["⟦", "⟧"], ["⦃", "⦄"], + ["⟪", "⟫"], + ["⦉", "⦊"], ["`", "`"], ["\"", "\""] ],