Skip to content

Autocomplete for Refinements#58

Merged
rcosta358 merged 11 commits intomainfrom
autocomplete
Feb 26, 2026
Merged

Autocomplete for Refinements#58
rcosta358 merged 11 commits intomainfrom
autocomplete

Conversation

@rcosta358
Copy link
Collaborator

@rcosta358 rcosta358 commented Feb 19, 2026

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

2026-02-19-16-52-10.mp4

@rcosta358 rcosta358 self-assigned this Feb 19, 2026
@rcosta358 rcosta358 added the enhancement New feature or request label Feb 19, 2026
@rcosta358 rcosta358 linked an issue Feb 19, 2026 that may be closed by this pull request
Copy link
Collaborator

@CatarinaGamboa CatarinaGamboa left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

looks great! sorry for the delay, you'll have to rebase

@rcosta358 rcosta358 merged commit e21b55f into main Feb 26, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement New feature or request

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Autocomplete suggestions with states and (this)

2 participants