Stream: Coq devs & plugin devs

Topic: Background diff tag hack

view this post on Zulip Maxime Dénès (Aug 23 2023 at 12:39):

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...

view this post on Zulip Gaëtan Gilbert (Sep 04 2023 at 12:47):

cc @Jim Fehrle

view this post on Zulip Jim Fehrle (Sep 04 2023 at 21:32):

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:

  1. highlight each Ppcmd_string and intervening Ppcmd_print_break (generating white space) individually.
  2. highlight appropriate subtrees. A bit tricky to code because a highlighted span may apply to parts of adjacent Pp.t subtrees that twould have to be tagged separately.
  3. Use spans

#3 seemed simplest to implement.

view this post on Zulip Jim Fehrle (Sep 04 2023 at 21:34):

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