diff --git a/vscode-lean4/language-configuration.json b/vscode-lean4/language-configuration.json index 9b1fa49a1..bc78770a5 100644 --- a/vscode-lean4/language-configuration.json +++ b/vscode-lean4/language-configuration.json @@ -145,7 +145,8 @@ ["\"", "\""], ["'", "'"], ["`", "`"], - ["*", "*"] + ["*", "*"], + ["$", "$"] ], "wordPattern": "([^!`~@$%^&*()\\-=+\\[{\\]}⟨⟩⦃⦄⟦⟧⟮⟯‹›<>\\\\|;:\",./\\s][^`~@$%^&*()\\-=+\\[{\\]}⟨⟩⦃⦄⟦⟧⟮⟯‹›<>\\\\|;:\",./\\s]*)", "onEnterRules": [