feat: make lean files in .lake and .elan read-only (#608)

This PR prevents users from accidentally editing dependencies in `.lake`
and `.elan` when jumping to them, e.g. using go-to-definition.

Author: mhuisi

vscode-lean4/package.json

@@ -1009,6 +1009,10 @@
             }
         ],
         "configurationDefaults": {
+            "files.readonlyInclude": {
+                "**/.lake/**/*.lean": true,
+                "**/.elan/**/*.lean": true
+            },
             "[lean4]": {
                 "editor.unicodeHighlight.ambiguousCharacters": false,
                 "editor.tabSize": 2,