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 ?
So, the magic happens in the v
.
(first letter of the implementation of yourpr_infos_list
)
let v n s = Ppcmd_box(Pp_vbox n,s)
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