Highlighting locations in lines with unicode on rich terminals

[gasche]

In #11899, @hhugo points out that our current approach of highlighting locations using ^^^^ on the line below is fragile in presence of unicode characters with a non-obvious display width.

$ cat c.ml
let (s : string) = "npiπππ" ^ 2
$ ocamlc -c c.ml
File "c.ml", line 1, characters 33-34:
1 | let (s : string) = "npiπππ" ^ 2
                                     ^
Error: This expression has type int but an expression was expected of type
         string

The discussion of #11899 clarifies that it seems unrealistic to be able to compute the "right" width at which to place the ^ on the line below (especially within the compiler distribution with a minimal library footprint).

For rich terminals, we propose instead to stick to location-highlighting formats that are "on-line" in the sense of being overlayed on the line: text font, weight or color, underlining, etc.

Proposal: use underlining to highlight the location in the quoted string.

This is what we use in the toplevel, but not (currently) in the "rich" error reporting format in batch mode.

[gasche]

(see #11918 for dumb terminals)

[gasche]

Using an on-line notation also simplifies the user-interface questions we have about multiline locations, namely, how to elide the prefix and suffix of the quoted lines that are not part of the location. We can just show them, but not highlighted. See #9116, #9118, #11678.

[gasche]

cc @Julow: reply here if you want to get this issue assigned to you :-)

[Julow]

I can have a look at both issues.

[gasche]

(No replying, no assigning, that's a limitation of the github interface.)

[gasche]

The asai library has a design document that explains their position with respect to unicode art in error messages;

https://redprl.org/asai/asai/design.html#unicode-art

The points made there are reminiscent of the discussion happening here.

(cc @favonia for cross-information, although there is nothing specific we are asking you to do here; of course help working on these topics is always welcome)

[favonia]

I'm glad that our notes help. :-) Your proposal in this GitHub issue is basically the same as our choice, for exactly the same reasons.

I see there are some complaints about tabs in #9116 and #9118. In case it's relevant, for control characters and other "bad" characters, we either expand them to spaces or replace them with � (Uchar.rep). Our current implementation expands a tab into a constant number of spaces regardless of its location. This could be relevant here because you probably do not want any control character to mess up the highlighting. Our (very inefficient) code is here: https://github.com/RedPRL/asai/blob/2ec78f8dc785ef60039902be21c901a2ddf7de8d/src/tty/UserContent.ml#L1-L22

Some further information: I'm planning to rewrite our built-in terminal renderer to abandon notty. Maybe I'll use @dbuenzli's fmt to handle colors? But I also want to use hyperlinks, which are supported on all modern "rich" terminal emulators. It's a shame that there is no reliable way to compose different handlers of semantic tags, even though the type Format.stag itself is an open variant type.

[dbuenzli]

I was never convinced by the tags approach which is totally uncompositional. I think that the ability for formatters to store arbitrary key-value data is the right way of solving the problem of adapting formatting functions to the output context (e.g. tty vs text, unicode art vs ASCII art etc.).

Note that nowadays that we have Type.Id it wouldn't be very hard to add this and it would be nice to get it upstream along with a few pre-defined keys like isatty (and if we are wild even functions for styled formatting).

In fmt I actually abuse semantic tags as storage for such an arbitrary key-value store :–)