Lean Processed Highlighter

Highlight proven (processed) regions of Lean 4 files in green, like VSRcoq.
Works on top of the official Lean 4 extension.

Quick start

Step	Action
1	Install Lean 4 + this extension
2	Open a `.lean` file — processed code turns green automatically
3	`Alt+↓` / `Alt+↑` — step through processed blocks manually
4	`Alt+R` — reset to follow the server again

Auto‑highlight — the proven prefix (from file start to the latest processed position) gets a translucent green background as Lean verifies your code.
Manual stepping — Alt+↓ / Alt+↑ move the "frontier" without moving code, letting you inspect the proof state at each step boundary.
Two step modes (toggle via Command Palette):
- Atomic — step through every incremental fragment the server reported (more granular).
- Merged — step through the server's merged processed ranges.
Reset (Alt+R) — back to auto‑follow.
Diagnostic output — open View → Output → "Lean Processed Highlighter" to see real‑time progress.

Shortcut	Command	Action
`Alt+↓`	`Lean4: Step Highlight Forward`	Next processed block
`Alt+↑`	`Lean4: Step Highlight Backward`	Previous / current block start
`Alt+R`	`Lean4: Reset Highlight To Server State`	Reset to auto‑follow

All commands are also available via Ctrl+Shift+P → Lean4: ....

ID	Title
`lean4Processed.toggle`	Toggle Processed Highlight
`lean4Processed.highlightNow`	Highlight Processed Region Now
`lean4Processed.stepForward` / `stepBackward`	Step Highlight Forward / Backward
`lean4Processed.reset` / `followServer`	Reset / Follow Server Progress
`lean4Processed.toggleStepMode`	Toggle Step Mode (Atomic / Merged)

MIT