🎨 Option to highligh text without ANSI control sequences

[favonia]

No description provided.

[mikeshulman]

Just wanted to add a note that this would be very useful for me. Narya now has a ProofGeneral mode which in general I'm quite happy with, but its error-reporting is less than ideal because the highlights are not visible. So often when I'm coding in ProofGeneral and I get an error, I have to switch back to the command-line to see the highlighted error that points out where in the line the error happened.

I don't know how you were thinking of doing this. One obvious option is the usual sort of ASCII underlining:

line with an error
             ^^^^^

But this only works in a monospace font, and I like to use variable-width fonts particularly for Unicode math characters. A fancier option would be to produce the output in some kind of markup language which any editor client could parse and display however it likes.

Or is the proper way to do this with #107, or with the LSP package?

[favonia]

@mikeshulman I'm not familiar with ProofGeneral. Does it put the output into a CompilationMode buffer so that compilation-error-regexp-alist would work? If so, perhaps we could output something that Emacs can directly understand? Otherwise, yes, we can implement #107.

[mikeshulman]

No, it uses its own proof-response-mode, but I should be able to customize Narya's derived version of that mode to do anything necessary. What sort of output were you thinking of?

[favonia]

@mikeshulman In principle, I and a few other key developers do not like using column numbers, which are confusing. However, if that's the only way, so be it. The format that Emacs should definitely accept is the GNU coding standard on errors.

[mikeshulman]

Why would column numbers be better than markup?

[favonia]

@mikeshulman I think markups are always better than column numbers, but I don't know whether ProofGeneral supports any. These are possible approaches, roughly from the best to the worst, in my opinion:

1. Use some built-in format supported by ProofGeneral to highlight the spans.
2. Generate Emacs Lisp code that defines a derived mode from proof-response-mode that supports custom highlighting and/or enables the ANSI coloring via e.g. ansi-color-compilation-filter.
3. In a way very similar to the above approach, generate Emacs Lisp code that somehow enables Emacs's Compilation Minor mode and output errors according to the GNU standard. (The downside is that this uses column numbers.)
4. Use LSP or other existing protocols, skipping ProofGeneral entirely.
5. Implement 💅 Implement a handler based on grace #107 (which does assume monospaced font to some degree).

Reading the documentation more, I realized Emacs (correctly) sets the TERM environment variable to dumb in a shell-mode and perhaps ProofGeneral inherits this convention. If so, then Narya (or more precisely, the Tty backend provided by asai) will detect this as "no ANSI coloring allowed" and avoid all control sequencing. To always enable ANSI coloring, you would have to do the following two things at once:

1. Use ansi-color-compilation-filter or other filters to enable ANSI coloring on the Emacs side, and
2. Change TERM to something else to hint the ability to handle ANSI coloring (recommended), or pass ~use_ansi:true to the display function.

@mikeshulman BTW, I'm surprised that your variable-width font display all digits (0, 1, 2, ...) with the same width. Or, are you talking about a duospaced font?

[mikeshulman]

I don't think PG supports markup directly, but I should be able to manage (2). Each prover already has its own derived modes, so I can try to turn on ansi color. Thanks for the suggestion.

What gave you the impression that my font displays all digits with the same width?

But actually, I have Emacs configured to use an ordinary monospace font for ordinary alphanumeric characters and a different variable-width font for fancier unicode characters.

[mikeshulman]

Wow, it works! Apparently ProofGeneral already has an (undocumented) configuration variable pg-insert-text-function that can be customized to call ansi-color-apply-on-region after inserting text. So that was amazingly easy.

I did have to use use_ansi, though, as I'm not sure how to change the value of TERM sent by ProofGeneral. Its response-mode inherits from scomint-mode, which appears to hardcode setting TERM=dumb in the function scomint-exec-1. Is setting TERM instead of passing use_ansi recommended just on the general principle that it's the caller's responsibility to inform the program whether it understands ANSI, or is there some more concrete potential problem I should be concerned about?

[favonia]

What gave you the impression that my font displays all digits with the same width?

Because I believe the outcome would be horrible otherwise. It seems your sophisticated setting avoided all the trouble. 😁

I did have to use use_ansi, though, as I'm not sure how to change the value of TERM sent by ProofGeneral. Its response-mode inherits from scomint-mode, which appears to hardcode setting TERM=dumb in the function scomint-exec-1. Is setting TERM instead of passing use_ansi recommended just on the general principle that it's the caller's responsibility to inform the program whether it understands ANSI, or is there some more concrete potential problem I should be concerned about?

It's just on the general principle that a program should not unconditionally force ANSI coloring. Narya might be one day used in an environment that really does not support ANSI coloring. (For example, maybe someone redirects its output to a file etc.) One common strategy is to implement the --color=ture/false/auto or --color flag and tell ProofGeneral to call narya --color=true or narya --color instead.

[mikeshulman]

Oh, Narya already has a special -proofgeneral flag that adjusts a bunch of other settings in ways that only make sense when interacting with PG, so I tied the unconditional use_ansi to that flag.

[favonia]

@mikeshulman That sounds like a very reasonable approach!

[favonia]

This is mostly solved by #175 that (1) uses French double quotation marks for ranges when ANSI is disabled, by default, and (2) allows library users to decide whatever quotation marks to use. I'm thus closing this issue.