Skip to content

Commit

Permalink
feat: provide more bracket support (#330)
Browse files Browse the repository at this point in the history
* feat: support for modified standard brackets

* feat: support for modified string literals

* feat: support for markdown enclosers on select

* change: remove `$[`, `]` as a bracket pair

* docs: create `language-configuration.md`
* remove markdown comment
  • Loading branch information
thorimur authored Mar 12, 2024
1 parent 37d2d73 commit 212cbd4
Show file tree
Hide file tree
Showing 2 changed files with 49 additions and 3 deletions.
27 changes: 27 additions & 0 deletions docs/language-configuration.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
This document serves as documentation for [`language-configuration.json`](/vscode-lean4/language-configuration.json).

See [the official VS code documentation](https://code.visualstudio.com/api/language-extensions/language-configuration-guide) for an overview of how `language-configuration.json` files work in general.

Section titles here are top-level fields in the JSON file, and link to their corresponding section in the official documentation.

## [`brackets`](https://code.visualstudio.com/api/language-extensions/language-configuration-guide#brackets-definition), [`autoClosingPairs`](https://code.visualstudio.com/api/language-extensions/language-configuration-guide#autoclosing), and [`surroundingPairs`](https://code.visualstudio.com/api/language-extensions/language-configuration-guide#autosurrounding)

All of these fields handle brackets in different ways.

* `brackets`: determines highlighting and selection
* `autoClosingPairs`: specifies which bracket pairs should prompt automatic insertion of a closing bracket upon typing the initial bracket
* `surroundingPairs`: specifies which brackets should surround highlighted content when typed (e.g. highlighting a term then typing <kbd>(</kbd> should surround the term with parentheses)

### Markdown

We include the following only in `surroundingPairs`:

```json
...
["`", "`"],
["*", "*"],
["_", "_"]
...
```

This means that you can highlight text in comments and italicize, bold, or code-format it easily by typing the respective marker(s). We don't want to use these as actual brackets or autoclosing pairs, however, due to their use in Lean code.
25 changes: 22 additions & 3 deletions vscode-lean4/language-configuration.json
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,12 @@
},
"brackets": [
["(", ")"],
["`(", ")"],
["``(", ")"],
["[", "]"],
["#[", "]"],
["@[", "]"],
["%[", "]"],
["{", "}"],
["⁅", "⁆"],
["⁽", "⁾"],
Expand Down Expand Up @@ -43,11 +48,19 @@
["[", "]"],
["{", "}"],
["「", "」"],
["\"", "\""]
["\"", "\""],
["s!\"", "\""],
["f!\"", "\""],
["m!\"", "\""]
],
"autoClosingPairs": [
["(", ")"],
["`(", ")"],
["``(", ")"],
["[", "]"],
["#[", "]"],
["@[", "]"],
["%[", "]"],
["{", "}"],
["⁅", "⁆"],
["⟮", "⟯"],
Expand Down Expand Up @@ -86,7 +99,10 @@
["{", "}"],
["「", "」"],
["/-", "-/"],
["\"", "\""]
["\"", "\""],
["s!\"", "\""],
["f!\"", "\""],
["m!\"", "\""]
],
"surroundingPairs": [
["(", ")"],
Expand Down Expand Up @@ -128,7 +144,10 @@
["{", "}"],
["「", "」"],
["\"", "\""],
["'", "'"]
["'", "'"],
["`", "`"],
["*", "*"],
["_", "_"]
],
"wordPattern" : "([^`~@$%^&*()\\-=+\\[{\\]}⟨⟩⦃⦄⟦⟧⟮⟯‹›<>\\\\|;:\",./\\s]+)"
}

0 comments on commit 212cbd4

Please sign in to comment.