search

aya-prover / aya-vscode

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

Work with new highlight data and library system #18

Closed imkiva closed 2 years ago

imkiva commented 2 years ago

Depends on aya-prover/aya-dev#245

ice1000 commented 2 years ago

We no longer need tokenFor for highlighting? Are they completely useless?

imkiva commented 2 years ago

We no longer need tokenFor for highlighting? Are they completely useless?

Yes. the tokenFor is from language server spec which lacks precise control of highlights (like we cannot highlight field projections) and it's not general. We now generate highlight colors just from our token type (like agda-mode on vscode)

ice1000 commented 2 years ago

bors is dead?

bors r+

bors[bot] commented 2 years ago

Build succeeded: