Stream: Coq devs & plugin devs

Topic: Formatting query results: About


view this post on Zulip Romain Tetley (Aug 23 2023 at 14:17):

So apparently the different sections of the result of an about query are separated using a "cut" which translates to a Ppcmd_print_break (0, 0). Done through this function:

let pr_infos_list l = v 0 (prlist_with_sep cut (fun x -> x) l)

In coqide and coqtop this seems to translate to line breaks. The spec from ocaml makes me feel like this should at least be a print_break (0, 1):
"pp_print_cut ppf () emits a 'cut' break hint: the pretty-printer may split the line at this point, otherwise it prints nothing."
I'm reimplementing formatting for VsCoq2 and currently this leads to a bad result line formatting.

Does anyone here know if the behaviour I'm describing is indeed the one that has been chosen ? Additionally, could you point me towards the code where this is done ?

view this post on Zulip Maxime Dénès (Aug 24 2023 at 07:35):

So, the magic happens in the v.

view this post on Zulip Maxime Dénès (Aug 24 2023 at 07:36):

(first letter of the implementation of yourpr_infos_list)

view this post on Zulip Maxime Dénès (Aug 24 2023 at 07:37):

let v n s = Ppcmd_box(Pp_vbox n,s)

view this post on Zulip Maxime Dénès (Aug 24 2023 at 07:37):

so it opens a vbox in OCaml format's jargon, which means that all line cuts will be interpreted as new lines


Last updated: Oct 13 2024 at 01:02 UTC