We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 1651749 commit 8499468Copy full SHA for 8499468
ProofWidgets/Component/MakeEditLink.lean
@@ -47,7 +47,7 @@ If `newSelection?` is absent, place the cursor at the end of the new text.
47
If `newSelection?` is present, select the range it specifies within `newText`.
48
See also `MakeEditLinkProps.ofReplaceRange'`. -/
49
def MakeEditLinkProps.ofReplaceRange (doc : Server.DocumentMeta) (range : Lsp.Range)
50
- (newText : String) (newSelection? : Option (String.Pos × String.Pos) := none) :
+ (newText : String) (newSelection? : Option (String.Pos.Raw × String.Pos.Raw) := none) :
51
MakeEditLinkProps :=
52
ofReplaceRange' doc range newText (newSelection?.map fun (s, e) =>
53
let ps := range.start.advance (newText.toSubstring.extract 0 s)
0 commit comments