This repository was archived by the owner on Apr 2, 2025. It is now read-only.
This repository was archived by the owner on Apr 2, 2025. It is now read-only.
Feature request: highlight proof placeholders ("sorry") #320
Description
"sorry" is highlighted with pink background in Isabelle.
This helps visually locate the unfinished holes in the proof.
It would be nice to have this feature in vscode/lean.
