# HG changeset patch # User wenzelm # Date 1483302386 -3600 # Node ID 07bf45283b92fc25bf7404caeb79b9f1193016de # Parent 4ad6d21545bd4c08fa7d65ba0b8c3873c4cec300 clarified file name; diff -r 4ad6d21545bd -r 07bf45283b92 src/Tools/VSCode/extension/isabelle-language.json --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/isabelle-language.json Sun Jan 01 21:26:26 2017 +0100 @@ -0,0 +1,16 @@ +{ + "brackets": [ + ["(", ")"], + ["[", "]"], + ["{", "}"], + ["<", ">"], + ["«", "»"], + ["‹", "›"], + ["⟨", "⟩"], + ["⌈", "⌉"], + ["⌊", "⌋"], + ["⦇", "⦈"], + ["⟦", "⟧"], + ["⦃", "⦄"] + ] +} diff -r 4ad6d21545bd -r 07bf45283b92 src/Tools/VSCode/extension/language-configuration.json --- a/src/Tools/VSCode/extension/language-configuration.json Sun Jan 01 20:24:19 2017 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,16 +0,0 @@ -{ - "brackets": [ - ["(", ")"], - ["[", "]"], - ["{", "}"], - ["<", ">"], - ["«", "»"], - ["‹", "›"], - ["⟨", "⟩"], - ["⌈", "⌉"], - ["⌊", "⌋"], - ["⦇", "⦈"], - ["⟦", "⟧"], - ["⦃", "⦄"] - ] -} diff -r 4ad6d21545bd -r 07bf45283b92 src/Tools/VSCode/extension/package.json --- a/src/Tools/VSCode/extension/package.json Sun Jan 01 20:24:19 2017 +0100 +++ b/src/Tools/VSCode/extension/package.json Sun Jan 01 21:26:26 2017 +0100 @@ -26,7 +26,7 @@ "id": "isabelle", "aliases": ["Isabelle"], "extensions": [".thy"], - "configuration": "./language-configuration.json" + "configuration": "./isabelle-language.json" } ], "configuration": {