Skip to content

Add Context Debugger#64

Open
rcosta358 wants to merge 20 commits intomainfrom
context-debugger
Open

Add Context Debugger#64
rcosta358 wants to merge 20 commits intomainfrom
context-debugger

Conversation

@rcosta358
Copy link
Collaborator

@rcosta358 rcosta358 commented Mar 7, 2026

This PR implements the context debugger for the webview, which shows the refinement aliases (globally), ghosts (by file), and variables (by file and scope) in the context.

  • When using a single-point cursor, shows all variables in scope until the cursor position
  • When using a cursor selection, shows all variables in scope within the selection
  • When clicking on a variable, highlights it in the editor
  • When a refinement or state refinement fails, shows the expected type in red after the turnstile (⊢)

Demo

Screen.Recording.2026-03-07.at.20.47.37.mp4

Depends on #159 from the liquidjava verifier.

@rcosta358 rcosta358 self-assigned this Mar 7, 2026
@rcosta358 rcosta358 added the enhancement New feature or request label Mar 7, 2026
@rcosta358 rcosta358 changed the title Context Debugger Add Context Debugger Mar 7, 2026
@rcosta358 rcosta358 requested a review from CatarinaGamboa March 7, 2026 21:44
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.

1 participant