Merge pull request #102 from larsk21/editor-word-separators

gebner · web-flow · commit cfe760c64605 · 2022-01-14T12:47:53.000+01:00
Add configuration default for `editor.wordSeparators`
diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json
@@ -380,7 +380,8 @@
 		"configurationDefaults": {
 			"[lean4]": {
 				"editor.unicodeHighlight.ambiguousCharacters": false,
-				"editor.tabSize": 2
+				"editor.tabSize": 2,
+				"editor.wordSeparators": "`~@$%^&*()-=+[{]}⟨⟩⦃⦄⟦⟧⟮⟯‹›\\|;:\",.<>/"
 			}
 		}
 	},

Original file line number	Diff line number	Diff line change
`@@ -380,7 +380,8 @@`
`380`	`380`	`"configurationDefaults": {`
`381`	`381`	`"[lean4]": {`
`382`	`382`	`"editor.unicodeHighlight.ambiguousCharacters": false,`
`383`		`- "editor.tabSize": 2`
	`383`	`+ "editor.tabSize": 2,`
	`384`	+ "editor.wordSeparators": "`~@$%^&*()-=+[{]}⟨⟩⦃⦄⟦⟧⟮⟯‹›\\\|;:\",.<>/"
`384`	`385`	`}`
`385`	`386`	`}`
`386`	`387`	`},`