This PR adds autocomplete for refinements using the context history from the verifier.
It suggests variables in scope, fields, ghosts, states, aliases, and keywords (this, old, return), only when inside a string within a LiquidJava annotation (except for the parameter msg).
To only show the variables in scope, we update the current position of the cursor when it moves and then filter variables that aren't either in scope of the current position or their declaration is after the current position.

Demo

Future Work

This still needs improvements, such as:

• Suggest parameters in method and parameter level refinements
• Suggest fields, ghosts and states in the class after this.
• Don't suggest ghosts/states from different classes (aliases are fine)
• Don't suggest return unless we are in a method level refinement
• Annotation-specific suggestions