animated gutter and actiongroup icons
Hi all, apologies if this question becomes too long or overly complicated. Just trying to figure out if I'm even in the right ballpark with all this -- and if it's even feasible this way.
I'm trying to write an Intellij plugin for a jar-based tool that analyzes code (proves it correct w.r.t some spec) and updates icons in the gutter accordingly with information as it comes back from a tool. However, I am having some trouble figuring out how communicate proof 'progress' via animated icons in the gutter.
I figure some initial screenshots illustrating what I'm trying to do (and where I currently am) might help, so here goes:
First I select the "prove program" action. This triggers the actionPerformed method in my corresponding "ProverAction extends AnAction" class. The first thing I do in actionPerformed is run the tool once (without proving yet!) to retrieve some initial information I want annotated in the gutter, resulting in this:
Once these VCs (proof obligations) are painted, actionPerformed then immediately invokes the prover the background which I want to result in updates to their appearance (based on whether or not they were proven, timed out, etc). One complicating wrinkle is that technically an arbitrary number of individual vcs can arise from a given line of code. So when you click the icon in the gutter, it merely brings up a context menu contain clickable, individual AnAction objects in a group (see picture three) -- which are the actual vcs..
As I mentioned, actionPerformed concludes by invoking the prover in the background (usingTask.Backgroundable). The tool/prover is given an implementation of a "proverlistener" that adds vcs to a container as they are proved -- the same instance of this listener object was also given to each individual VC action in the hopes that I could use it to dynamically affect the appearance of each indivdual VC menu action.. (I messed with this listener in the "update" method for each action, but I don't think that's going to quite do it for the goals below..)
Here's what I would like to have happen:
1. I would like to have the orange VC buttons in the gutter doing some kind of animation while the prover is running -- indicating that one or more of its submenu VCs has not yet finished proving. The orange vc gutter icon should change to green once all sub vcs are proven -- red otherwise.
2. Also, it would be nice (preferable) to have each of the individual VC actions within each submenu also doing an animation while they are being proven (or at least in line to being proven), green when done, etc. For instance, in the previous picture, while "VC #1: restores ..." is showing done (green), it would be nice to have a spinning circle next to it *before* it finishes for the sake of user feedback, etc.
Here's some pseudocode to try to communicate how I'm currently doing things.. Right now I have the basics somewhat working. I can for instance, change a vc gutter icon's appearance based on state of its sub actions (whether they are all proven, etc), and I can change the icon on each individual vc based on whether or not its proven (via its "update" method).. but the real difficulty I'm having is in trying to get all of this animating in line with the process running in the background.
I don't have much experience at all with processes and threads in IntelliJ so please try to excuse my ignorance. If you prefer to just skip this and look at the actual code I'm summarizing, you can find it all in this file:
public class ProverAction extends AnAction {
public void actionPerformed(AnActionEvent e) {
/* ... retrieve editor, project, do some simple sanity checks, etc */
//this is passed into the tool and filled up with results as the prover gets to them, initially it's of course empty
MyProverListener pl = new MyProverListener();
//this produces a raw collection of VC objects in vco that I use to make all the menu actions, etc in the subsequent steps
VCOutputFile vco = generateVCs(virtualFile, editor, project);
if (vco == null) return;
//now present the vcs
MarkupModel markup = editor.getMarkupModel();
Map<Int, List<VC>> byLineNum = vco.getVCsClumpedByLineNumber();
for (Map.Entry<Int, List<VC>> vcsByLine : byLineNum.entrySet()) {
List<VC> actionsPerVC = new ArrayList<>();
for (VC vc : vcsByLine.getValue()) {
//pass my prover listener into each individual vc menu action.
actionsPerVC.add(new ProverVCAction(listener, vc.getNumber(), vc.getExplanation());
}
//create a highlighter, and add "actionsPerVC" as popup menue actionGroup
//for the gutterIconRenderer... *see code in the git link before this code listing*
}
//finally, invoke the prover
List<String> args = new ArrayList<>();
args.add(virtualFile.getPath());
args.add("-lib");
...
args.add("-prove");
RESOLVECompiler compiler = new RESOLVECompiler(args.toArray(new String[args.size()]));
compiler.addProverListener(pl);
ProgressManager.getInstance().run(new Task.Backgroundable(project, "Description") {
@Override
public void run(@NotNull final ProgressIndicator progressIndicator) {
compiler.processCommandLineTargets();
}
});
}
Thanks for reading.
Please sign in to leave a comment.
There's no support currently for animated icons in editor's gutter. You can probably try implementing it by changing highlighter's icon renderer repetitively, I'm not sure though whether a reasonable performance can be achieved in that way.