search

aya-prover / aya-vscode

~ VSCode extension for Aya Prover
GNU General Public License v3.0
7 stars 2 forks source link

How to add new commands? #6

Closed ice1000 closed 3 years ago

ice1000 commented 3 years ago

I wanna implement a command like this:

@imkiva need your help!!

imkiva commented 3 years ago
  • VSCode sends the LSP an instance of some subtype of org.eclipse.lsp4j.TextDocumentPositionParams (done in this client -- Idk how to do it, I need help!)

The client-side should send a named json request (for example aya/load here): https://github.com/aya-prover/aya-vscode/blob/8d1f833377d9e5ac68e6a870f33b00afc06c0fcb/src/server-daemon.ts#L126-L127

The server side should register a json request handler with the same name in AyaServer:

https://github.com/aya-prover/aya-dev/blob/3ee50df7ed6e8774491bb453cc342e9fcad30fe7/lsp/src/main/java/org/aya/lsp/server/AyaServer.java#L22-L26

imkiva commented 3 years ago
  • LSP finds an instance of Doc (which, probably we need to convert to plain text before sending to VSCode, but maybe HTML also works?) and a range (done in the compiler, I know how to do it, I don't need help!)

Yes. HTML works.

imkiva commented 3 years ago
  • VSCode selects the provided range and show the Doc somehow, maybe similar to how GHC-Simple shows the type of expressions (done in this client -- Idk how to do it, I need help!)

idk either. But I found this SO thread: https://stackoverflow.com/questions/47250698/set-selection-range-in-the-visual-studio-code-document

re-xyr commented 3 years ago

Yes. HTML works.

I thought they were sanitized away?

maybe similar to how GHC-Simple shows the type of expressions

But ghc-simple gives plaintext code annotations.

ice1000 commented 3 years ago

But ghc-simple gives plaintext code annotations.

Why not do better if we can

re-xyr commented 3 years ago

I think that kind of annotation (next to code) accepts only plaintext.

ice1000 commented 3 years ago

I think that kind of annotation (next to code) accepts only plaintext.

Then we'll just use plaintext backend of Doc, I think it'll be fine

ice1000 commented 3 years ago

OMG turns out we have more problems (now we have a problem factory)

ice1000 commented 3 years ago

I added computeNF, can you add vscode support for it too @imkiva

Btw, I've realized I cannot obtain the source code range for a CallTerm. So sad.

ice1000 commented 3 years ago

@ice1000 I found an unreliable way to do this

imkiva commented 3 years ago

I added computeNF, can you add vscode support for it too @imkiva

now vscode supports computeNF

ice1000 commented 3 years ago

Ok, closing.