When using the Lambdapi VS Code extension, the goal view stops updating and no longer displays the current proof state as soon as there is an unfinished or malformed line in the proof script. This occurs whether the line is partially written (e.g. a have keyword that requires arguments) or just contains nonsensical text.
For instance, consider the following file:
1 require open Stdlib.Set Stdlib.Prop;
2
3 symbol example x : π (x ⇒ ⊤) ≔
4 begin
5 assume x h;
6 have
7 end;
Line 6 (have) is incomplete and even in line 5, the goal can no longer be displayed (Instead, "No goals" is shown in the panel).
Attached is a minimal Lambdapi package reproducing the issue.
issueWithGoalDisplay.zip