code-lenses #33

Merged

michael merged 36 commits from code-lenses into main 2026-04-22 07:34:14 +02:00

Conversation 0 Commits 36 Files changed 19 +1341 -1604

michael commented 2026-04-22 07:33:49 +02:00

Owner

• Copy link

No description provided.

michael added 36 commits 2026-04-22 07:33:49 +02:00

Added a code-lens which for now is in a static position and sends the user to a static spot 93f8249a1a

Removed code to automatically register commands via the extention as that is already supported in the language server 3361c36b50

Removed template code lens 9b7576a4d5

Added auto generated id when creating new contracts 481373057c

Made go to proof not go to a static file, but to <current_file>_proofs.v, position in file is still temporarily static e8980445fc

Made completion of the keyword "id" inside contracts also generate a uuid f9c43d1a46

Merge remote-tracking branch 'origin/main' into code-lenses 5a07d48bb7

start cooking with documents with subsections f839d6f399

doctor up 213bf0478a

asyncify doctor d1ba2e2930

rename section to cut 660641d1d9

add post_change function to CutDoctor trait 7f26a1dd1f

add program to new skeleton f28d5e0590

forward diagnostics from vsrocqtop 8717f18a98

ghetto generate proof on save 09de86097b

clean up contracts.rs 9e6801c61f

Added a code-lens which for now is in a static position and sends the user to a static spot 7c37dd3f37

Removed code to automatically register commands via the extention as that is already supported in the language server 439bfdc4e0

Removed template code lens 08a65f5fd2

Added auto generated id when creating new contracts 7220710824

Made go to proof not go to a static file, but to <current_file>_proofs.v, position in file is still temporarily static 7234b616df

remove log e128e75014

rm old skeleton 59036a6de5

Merge branch 'code-lenses' of https://git.marfavi.com/code2rocq/imp2rocq into code-lenses f98d04043b

Added id to the extracted skeleton spec 44b3ee879c

Merge remote-tracking branch 'origin/refactor-documents' into code-lenses 21077a93c5

vsrocq shouldnt override other diagnostics f726edcb4e

ghetto fix that glue-ls (probably vsrocqtop client child process) isnt forcefully shut down 6eccfac412

made id be put into the proof file 467bf254e4

changed id TAB uuid, to id SPACE uuid d848c04cbf

update id cut in skeleton c4e81676ff

Merge remote-tracking branch 'origin/refactor-documents' into code-lenses c51b1c8701

Fixed crash if vsrocqtop was not installed 413d309512

Code lenses now include an argument with the id in the codelens if it exists dea5059134

Implemented go to proof 6db0ac9040

Added fix for \r\n lineendings d6cae38f8b

michael merged commit c1042adf2e into main 2026-04-22 07:34:14 +02:00

michael deleted branch code-lenses 2026-04-22 07:34:14 +02:00

michael referenced this pull request from a commit 2026-04-22 07:34:16 +02:00

code-lenses (#33)

Commenting is not possible because the repository is archived.

Reviewers

No reviewers

Labels

Clear labels

No items

No labels

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

1 participant

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

code2rocq/imp2rocq!33

No description provided.