I was wondering: why do we hack pp data here: https://github.com/coq/coq/blob/854d46bdb7699dc08410690d80ffdf107ce641d6/lib/pp_diff.ml#L158 ?
The normal representation of a removed area would be something like
Pp_tag ("removed-bg", pp) but instead we emit
Pp_tag("start_removed_bg", Pp_string "") ++ pp ++ Pp_tag("end_removed_bg", Pp_string "").
Why is this hack needed?
IDEs who want to convert
Pp.t to HTML are probably going to have to implement the reverse transformation...
cc @Jim Fehrle
Hard to recall exactly what I was thinking 5+ years ago when I wrote this. It was my first nontrivial PR for Coq. I believe I wanted each diff tag to contain only a single Ppcmd_string, but I don't recall why this was important. I'm not certain the PG, Coqtail, CoqIDE, coqtop, etc. code is written to handle nested tags, though if I change this code to
tag (diff_tag ^ ".bg") pp, it looks OK in CoqIDE.
Having tags like
start_removed_bg fits pretty well with the underlying diff algorithm. I suggest not trying to change this, which probably means there's no need to change the lines you highlight.
To highlight a given span of tokens, there are 3 design alternatives:
#3 seemed simplest to implement.
BTW, how will vsCoq2 decide where to split lines? Pp.t did that reasonably well for many but not all cases. (Not so easy to automatically split in ways humans will like.)
Last updated: Nov 29 2023 at 21:01 UTC