code action behaviour?

Stream: lean4

[Siddhartha Gadgil]

I was experimenting with the (low level) code actions. This is very nice, especially that lazy actions are supported.

But there was one piece of unexpected behaviour and a related question regarding the examples in the codeaction.lean test file.

• I would have guessed that the code actions would replace the selected token with "Hello!!!" or the directory, as it seemed the range should be for the syntax object and this should be replaced by the new text. Instead they are inserted.
• And the question: in a real case, the inserted text will depend on the text in the range. How do I access this?

@Edward Ayers @Gabriel Ebner are there some examples I should look at?

[Edward Ayers]

Hello! There is an example of usage in the tests which it sounds like you found. You can get it to replace text by setting the range field in the TextEdit object. To determine the range of text that needs to be replaced you need to get the Syntax node of the text.

[Edward Ayers]

With Lean.Syntax.getRange?

[Edward Ayers]

Recovering an expression or piece of syntax from a document position can be a little involved, but the way to do it is to find a snapshot for a given position and then search the InfoTree to find what you are looking for. There are lots of examples of this in RequestHandling.lean

[Edward Ayers]

Also Lean.Syntax.getRange? will give you a Lean range, but this needs to be converted to an LSP range using leanPosToLspPos

[Siddhartha Gadgil]

I take it that the starting point should be to use params.range to get an LSP range and convert this to a Lean range. Is that correct?

[Edward Ayers]

yes

[Siddhartha Gadgil]

Thanks. Will experiment and ask again for any questions.

[Siddhartha Gadgil]

Been digging through the source code but am asking as there may be an easy answer: how do I get the contents of the current file?

[Siddhartha Gadgil]

With position as above which can be converted.

[Siddhartha Gadgil]

I do see a function readDoc. However this involves a request context. Can I call it when defining a code-action?

[Sebastian Ullrich]

I think you can retrieve the request context in the eager part

[Siddhartha Gadgil]

I see many ways to get a DocumentUri. Is there a function that gets the actual document from this?

[Edward Ayers]

let doc ← readDoc
doc.meta.uri

[Edward Ayers]

doc.meta.text has the actual sourcetext somewhere

[Siddhartha Gadgil]

I mean the other way. CodeActionParams has the uri and the identifiers. I need the new text as a function of the current file.

[Siddhartha Gadgil]

In an IO context readDoc does not work.

[Joachim Breitner]

I’d also like to use readDoc, but in the Elaborator monad (maybe with a piece of Syntax to locate the doc), so a suggestion here is welcome :-)

[Edward Ayers]

You can pass in the RequestContext as a closure

[Siddhartha Gadgil]

Edward Ayers said:

You can pass in the RequestContext as a closure

Can you give an example, say within the lazy part of the codeactions.lean file.

[Siddhartha Gadgil]

I want the inserted text to depend on the current text.

[Siddhartha Gadgil]

I don't know how to get the RequestContextfrom the CodeActionParams

[Siddhartha Gadgil]

It seems to me that it should be common for code-actions to depend on the current text. If I follow the code in the definitions I end up with TextEdit which asks for the new text, but not as a function of the current text.

[Edward Ayers]

@[codeActionProvider]
def xyz : CodeActionProvider := fun params snap => do
  let rc : RequestContext ← read
  let ca : CodeAction := {
    title := "xyz"
  }
  let lazy : RequestM CodeAction := do
        -- this is a requestM
        let doc ← RequestM.readDoc
        return ca

  return #[{
    eager := ca
    lazy? := some <| (EIO.toIO (fun x => x.message)) <| ReaderT.run lazy rc
  }]

[Edward Ayers]

I admit this is quite clunky

[Siddhartha Gadgil]

Thanks a lot.

[Sebastian Ullrich]

Joachim Breitner said:

I’d also like to use readDoc, but in the Elaborator monad (maybe with a piece of Syntax to locate the doc), so a suggestion here is welcome :-)

@Edward Ayers This makes me wonder whether elaborators really should be in charge of adding widgets. I'm imagining an alternative design where widgets are created by server handlers triggered by nodes in the info tree (perhaps containing data added by elaborators specifically for widget visualization). This would have the advantage that not only does the widget creation code have access to server data, you can also add widgets for existing elaborators, e.g. +/- buttons for any elabNumLit node.

[Anand Rao]

Edward Ayers said:

Also Lean.Syntax.getRange? will give you a Lean range, but this needs to be converted to an LSP range using leanPosToLspPos

Is there a similar function from LspPos to String.Pos? I am trying to get the user's cursor position as a String.Pos. So far I have been using _snap.beginPosas a reasonable approximation, but in my use case it would be better to have the actual position. I believe params.range starts and ends at the same position when nothing is selected, so I was wondering if I could just use that position (which is an LspPos) to get a String.Pos.

[Edward Ayers]

I think lspPosToUtf8Pos and toPosition should do it