Hi,
We are trying to switch proofgeneral/coq to an xml protocol so I
wouldn't rely on ANSI escape codes but rather on xml term decoration
if I were to implement such a feature.
And by the way proofgeneral already has term highlighting based on
regexps (in goals and response buffers too) so I am
No at all; the ansi-color module in Emacs can take care of that easily.
Clément.
On 2018-01-24 01:06, Jim Fehrle wrote:
> Hi,
>
>
>
> How difficult would it be for Proof General to support ANSI escape codes
> (used to set color, bold, underline, etc.) embedded in the output of a proof
>
> How difficult would it be for Proof General to support ANSI escape codes
> (used to set color, bold, underline, etc.) embedded in the output of a proof
> assistant?
Depends on the details, but you can try to simply add a call to
`ansi-color-apply-on-region compilation-filter-start` right after
