Skip to content

feat: indent on enter after starting a focus block#328

Merged
mhuisi merged 3 commits intoleanprover:masterfrom
thorimur:indent-focus-block-rule
Mar 13, 2024
Merged

feat: indent on enter after starting a focus block#328
mhuisi merged 3 commits intoleanprover:masterfrom
thorimur:indent-focus-block-rule

Conversation

@thorimur
Copy link
Copy Markdown
Contributor

@thorimur thorimur commented Sep 21, 2023

This PR adds the following to language-configuration.json to cause indentation after starting a focus block (·):

    "onEnterRules" : [
        {
            // Indent focus blocks
            "beforeText" : "^\\s*(·|\\.)\\s.*$",
            "action" : { "indent" : "indent" }
        }
    ]

Now, hitting enter after intro x yields

constructor
· intro x
  | <-- cursor ends up here

See Zulip.


Note: there are some cases where this will produce the incorrect indentation, e.g.

  · have : Foo := by
    | <-- cursor will be here

  · have : Foo := by
      | <-- cursor should be here

but handling EOL tokens like by is done in #329 .

Comment thread vscode-lean4/language-configuration.json Outdated
* remove corresponding comment from json
@mhuisi mhuisi merged commit 20b5310 into leanprover:master Mar 13, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants