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 CSS]. 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 them. 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. E. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
