DARe Support - Githubissues

LonMcGregor / VS-Code-Language-Server-for-Dafny

VS Code Dafny Language Server with Tactics Support

MIT License

0 stars 1 forks source link

DARe Support #3

Open LonMcGregor opened 6 years ago

LonMcGregor commented 6 years ago

[x] Prompt to remove unneeded annotations
[x] Remove current/all in method/all in file
[ ] Polish this feature

LonMcGregor commented 6 years ago

Now have basic way of reporting that an annotation should be removed

LonMcGregor commented 6 years ago

use a https://code.visualstudio.com/docs/extensionAPI/vscode-api#_a-namecodeactionaspan-classcodeitem-id567codeactionspan

LonMcGregor commented 6 years ago

Initial support now possible. needs further refinement

LonMcGregor commented 6 years ago

Some extra fixes:

[x] On removal of whole line, also remove semi and newlines
[x] Find some examples to test rewriting instead of just removal
[x] Remove code action once diagnostics go away

LonMcGregor commented 6 years ago

More complex solution is required to replace calc{}s for example

LonMcGregor commented 6 years ago

Test (Removal, simplification) of (Assert, invariant, decreases, lemma call, calc)

[x] R A
[ ] R I
[ ] R D
[x] R L
[x] R C
[ ] S A
[ ] S I
[ ] S D
[ ] S L
[x] S C

LonMcGregor commented 6 years ago

[x] Rename references to Shorty

hailzzx commented 4 years ago

Hi, I am doing my final year project, with the aim of simplify the annotations in dafny VScode extension. I think you did a really awesome thing but I am now struggling with it. I really need some help, thanks a lot.