Re: [PG-devel] Proof General's ability to interpret ANSI escape code from a proof assistant
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 not really sure what we would gain anyway. Best, P. 2018-01-24 7:06 GMT+01:00 Jim Fehrle : > 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 > assistant? > > > > (I’m getting started on making a few enhancements to Coq. It’s been a long > time since I used emacs. I’ve not used Proof General at all.) > > > > Thanks, > > > > Jim > > > ___ > ProofGeneral-devel mailing list > ProofGeneral-devel@inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Proof General's ability to interpret ANSI escape code from a proof assistant
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 > assistant? > > > > (I’m getting started on making a few enhancements to Coq. It’s been a long > time since I used emacs. I’ve not used Proof General at all.) > > > > Thanks, > > > > Jim > > > > ___ > ProofGeneral-devel mailing list > ProofGeneral-devel@inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel > signature.asc Description: OpenPGP digital signature ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Proof General's ability to interpret ANSI escape code from a proof assistant
> 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 inserting the new text. Stefan ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
