Hi Jim,

"Jim Fehrle" <jfeh...@sbcglobal.net> writes:

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

Sorry for the late reply, let me add a few brief comments.

Much in the line of what Pierre said, in the Coq side we are leaning
towards using an internal document model which roughly corresponds to a
subset of HTML.

That way, the document can be further processed by different backends
[with atom / vscode / jscoq doing basically almost nothing aside from

What emacs should receive is still an open question, I think that from
the code side there is no problem in serving emacs the format they
prefer, including the console rendering if that's more convenient for

The new protocol requires the UI to include the output format desired,
for example:

`(Query ((pp ((pp_format PpAnsi)))) Goals)`

so it is not a big deal for clients to adapt.

ProofGeneral-devel mailing list

Reply via email to