From ca4fea494759ebff6ca10d1507e608745843474e Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 12 Dec 2023 21:58:38 +0100 Subject: [PATCH 1/4] feat: snippet extension --- src/Lean/Data/Lsp/Basic.lean | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/src/Lean/Data/Lsp/Basic.lean b/src/Lean/Data/Lsp/Basic.lean index f0baf7b6deee..28661219e810 100644 --- a/src/Lean/Data/Lsp/Basic.lean +++ b/src/Lean/Data/Lsp/Basic.lean @@ -78,6 +78,18 @@ structure Command where arguments? : Option (Array Json) := none deriving ToJson, FromJson +/-- A snippet string is a template which allows to insert text +and to control the editor cursor when insertion happens. + +A snippet can define tab stops and placeholders with `$1`, `$2` +and `${3:foo}`. `$0` defines the final tab stop, it defaults to +the end of the snippet. Variables are defined with `$name` and +`${name:default value}`. Also see +[the full snippet syntax](https://code.visualstudio.com/docs/editor/userdefinedsnippets#_creating-your-own-snippets). -/ +structure SnippetString where + value : String + deriving ToJson, FromJson + /-- A textual edit applicable to a text document. [reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textEdit) -/ @@ -87,6 +99,22 @@ structure TextEdit where range : Range /-- The string to be inserted. For delete operations use an empty string. -/ newText : String + /-- If this field is present and the editor supports it, + `newText` is ignored + and an interactive snippet edit is performed instead. + + *Note* that this is a Lean-specific extension to the LSP standard, + so `newText` should still be set to a correct value + as fallback in case the editor does not support this feature. + + *Note* that a snippet edit can always be performed as a normal text edit. + In VSCode, this will happen when no matching editor is open or when a workspace edit + contains snippet edits for multiple files. In that case only those that match the active editor + will be performed as snippet edits and the others as normal text edits. -/ + /- NOTE: Similar functionality may be added to LSP in the future: + see [issue #592](https://github.com/microsoft/language-server-protocol/issues/592). + If such an addition occurs, this field should be deprecated. -/ + leanExtSnippet? : Option SnippetString := none /-- Identifier for annotated edit. `WorkspaceEdit` has a `changeAnnotations` field that maps these identifiers to a `ChangeAnnotation`. From 95080448e0f43732971226491f2ed67810a1f9ad Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Thu, 14 Dec 2023 19:09:34 +0100 Subject: [PATCH 2/4] doc: address comment --- src/Lean/Data/Lsp/Basic.lean | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/Lean/Data/Lsp/Basic.lean b/src/Lean/Data/Lsp/Basic.lean index 28661219e810..c63c938c5788 100644 --- a/src/Lean/Data/Lsp/Basic.lean +++ b/src/Lean/Data/Lsp/Basic.lean @@ -103,14 +103,12 @@ structure TextEdit where `newText` is ignored and an interactive snippet edit is performed instead. - *Note* that this is a Lean-specific extension to the LSP standard, + This is a Lean-specific extension to the LSP standard, so `newText` should still be set to a correct value as fallback in case the editor does not support this feature. - - *Note* that a snippet edit can always be performed as a normal text edit. - In VSCode, this will happen when no matching editor is open or when a workspace edit - contains snippet edits for multiple files. In that case only those that match the active editor - will be performed as snippet edits and the others as normal text edits. -/ + Even editors that support snippets may not always use them; + for instance, if the file is not already open, + VS Code will perform a normal text edit in the background instead. -/ /- NOTE: Similar functionality may be added to LSP in the future: see [issue #592](https://github.com/microsoft/language-server-protocol/issues/592). If such an addition occurs, this field should be deprecated. -/ From 72d30bbdfc56116c5a6c6763c88ffcd3b29bbb41 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Fri, 15 Dec 2023 23:33:34 +0100 Subject: [PATCH 3/4] doc: update snippet docs Co-authored-by: David Thrane Christiansen --- src/Lean/Data/Lsp/Basic.lean | 39 +++++++++++++++++++++++++++--------- 1 file changed, 30 insertions(+), 9 deletions(-) diff --git a/src/Lean/Data/Lsp/Basic.lean b/src/Lean/Data/Lsp/Basic.lean index c63c938c5788..5cef48565af2 100644 --- a/src/Lean/Data/Lsp/Basic.lean +++ b/src/Lean/Data/Lsp/Basic.lean @@ -78,14 +78,34 @@ structure Command where arguments? : Option (Array Json) := none deriving ToJson, FromJson -/-- A snippet string is a template which allows to insert text -and to control the editor cursor when insertion happens. - -A snippet can define tab stops and placeholders with `$1`, `$2` -and `${3:foo}`. `$0` defines the final tab stop, it defaults to -the end of the snippet. Variables are defined with `$name` and -`${name:default value}`. Also see -[the full snippet syntax](https://code.visualstudio.com/docs/editor/userdefinedsnippets#_creating-your-own-snippets). -/ +/-- A snippet is a string that gets inserted into a document, +and can afterwards be edited by the user in a structured way. + +Snippets contain instructions that +specify how this structured editing should proceed. +They are expressed in a domain-specific language +based on one from TextMate, +including the following constructs: +- Designated positions for subsequent user input, + called "tab stops" after their most frequently-used keybinding. + They are denoted with `$1`, `$2`, and so forth. + `$0` denotes where the cursor should be positioned after all edits are completed, + defaulting to the end of the string. + Snippet tab stops are unrelated to tab stops used for indentation. +- Tab stops with default values, called _placeholders_, written `${1:default}`. + The default may itself contain a tab stop or a further placeholder + and multiple options to select from may be provided + by surrounding them with `|`s and separating them with `,`, + as in `${1|if $2 then $3 else $4,if let $2 := $3 then $4 else $5|}`. +- One of a set of predefined variables that are replaced with their values. + This includes the current line number (`$TM_LINE_NUMBER`) + or the text that was selected when the snippet was invoked (`$TM_SELECTED_TEXT`). +- Formatting instructions to modify variables using regular expressions + or a set of predefined filters. + +The full syntax and semantics of snippets, +including the available variables and the rules for escaping control characters, +are described in the [LSP specification](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#snippet_syntax). -/ structure SnippetString where value : String deriving ToJson, FromJson @@ -103,7 +123,8 @@ structure TextEdit where `newText` is ignored and an interactive snippet edit is performed instead. - This is a Lean-specific extension to the LSP standard, + The use of snippets in `TextEdit`s + is a Lean-specific extension to the LSP standard, so `newText` should still be set to a correct value as fallback in case the editor does not support this feature. Even editors that support snippets may not always use them; From c85e05181f1f411ce5a62eb24c8403f6155b57d0 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Wed, 20 Dec 2023 10:13:27 +0100 Subject: [PATCH 4/4] doc: release note --- RELEASES.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/RELEASES.md b/RELEASES.md index e2c2e1e72fa5..47c52e8794e1 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -36,6 +36,8 @@ v4.5.0 (development in progress) +termination_by _ x => hwf.wrap x ``` +* Support snippet edits in LSP `TextEdit`s. See `Lean.Lsp.SnippetString` for more details. + v4.4.0 ---------