Skip to content

Commit

Permalink
feat: indent on enter after starting a focus block (#328)
Browse files Browse the repository at this point in the history
* feat: indent on enter after starting a focus block

* docs: create `language-configuration.md`
* remove corresponding comment from json
  • Loading branch information
thorimur authored Mar 13, 2024
1 parent 5bba180 commit 20b5310
Show file tree
Hide file tree
Showing 2 changed files with 28 additions and 1 deletion.
21 changes: 21 additions & 0 deletions docs/language-configuration.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,27 @@ See [the official VS code documentation](https://code.visualstudio.com/api/langu

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

## [`onEnterRules`](https://code.visualstudio.com/api/language-extensions/language-configuration-guide#on-enter-rules)

This field specifies a list of rules which determine how lines should be indented when the user presses <kbd>Enter</kbd>. When the text in a line before the cursor is matched by the regex specified in a rule's `beforeText`, that rule's `action` is applied on <kbd>Enter</kbd>.

### Focus blocks

```json
{
"beforeText" : "^\\s*(·|\\.)\\s.*$",
"action" : { "indent" : "indent" }
}
```

This rule ensures that hitting enter after starting a focus block during a tactic sequence produces a line within that focus block. I.e.,

```
constructor
· intro x| <-- hit enter here
| <-- cursor ends up here
```

## [`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.
Expand Down
8 changes: 7 additions & 1 deletion vscode-lean4/language-configuration.json
Original file line number Diff line number Diff line change
Expand Up @@ -149,5 +149,11 @@
["*", "*"],
["_", "_"]
],
"wordPattern" : "([^`~@$%^&*()\\-=+\\[{\\]}⟨⟩⦃⦄⟦⟧⟮⟯‹›<>\\\\|;:\",./\\s]+)"
"wordPattern" : "([^`~@$%^&*()\\-=+\\[{\\]}⟨⟩⦃⦄⟦⟧⟮⟯‹›<>\\\\|;:\",./\\s]+)",
"onEnterRules" : [
{
"beforeText" : "^\\s*(·|\\.)\\s.*$",
"action" : { "indent" : "indent" }
}
]
}

0 comments on commit 20b5310

Please sign in to comment.