search

coq / vscoq

Visual Studio Code extension for Coq
MIT License
335 stars 68 forks source link

Command Inspect output is missing a line break #852

Open ybertot opened 2 months ago

ybertot commented 2 months ago

Inspect <n>. is supposed to display n elements, like the results of Search. If one puts an Inspect command in the middle of the script, the results is displayed in the message window, but it is not properly indented.

Here is a small reproducing example:

Definition two := 2.
Definition three := 3.
Inspect 2.

The output is two : natthree : nat in the message window, while it should be displayed on two lines.

Durbatuluk1701 commented 3 weeks ago

Seems like this may have been a bug in Coq that was fixed in 8.20: image However, running VsCoq with 8.20 we get two : nat three : nat: image

Not sure if this new form is acceptable, but if it isn't I feel like maybe this is coming from outside VsCoq?

We currently receive back the two Pp separated by a [ "Ppcmd_print_break", 1, 0 ], VsCoq chooses to make this a single space while coqtop turns the same thing into a newline? (To be honest I do not completely understand Ppcmd_print_break x y; is x a required amount of any type of space between and y horizontal offset? If so, a return of Ppcmd_print_break 1 0 for something we want new lines between seems incorrect)