Skip to content
Snippets Groups Projects
Commit 5a8aac0c authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[ivette/wp] improve menus

parent 3c2ad9e3
No related branches found
No related tags found
No related merge requests found
...@@ -50,12 +50,22 @@ function addStartProofMenus( ...@@ -50,12 +50,22 @@ function addStartProofMenus(
): void { ): void {
const { marker, kind } = attr; const { marker, kind } = attr;
switch (kind) { switch (kind) {
case 'STMT':
case 'LFUN': case 'LFUN':
case 'DFUN': case 'DFUN':
menu.push({
label: `Prove function using WP`,
onClick: () => Server.send(WP.startProofs, marker)
});
return;
case 'STMT':
menu.push({
label: `Prove statement annotations using WP`,
onClick: () => Server.send(WP.startProofs, marker)
});
return;
case 'PROPERTY': case 'PROPERTY':
menu.push({ menu.push({
label: `Generate WP Goals`, label: `Prove property using WP`,
onClick: () => Server.send(WP.startProofs, marker) onClick: () => Server.send(WP.startProofs, marker)
}); });
return; return;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment