aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-21 15:11:23 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-23 14:37:20 +0200
commit59bb9b37c58e8b5f8d009d598e949aa995e6973e (patch)
tree5df6f98dfc385964a4e493b80de1a3190f9a67d6 /toplevel
parentc86c6558fcf7f8dc4a17aceed24f68f756f28ea9 (diff)
[toplevel] [emacs] Don't quote errors in emacs mode.
In 8.6 + emacs, errors were quoted sometimes with special markers (e.g. `Print Module foo.` for a non-existing `foo`) In 8.7 we uniformized error handling and now all errors are quoted, however, this behavior confuses emacs as it seems that the quotes are meant to be applied only to warnings. We thus reflect the de-facto situation, removing quoting for errors and updating the code so it is clear that the quoter is a warnings quoter. We also update the warnings quoter to use a warning tag instead of a non-printable char. This fixes ProofGeneral for trunk users. c.f. https://github.com/ProofGeneral/PG/issues/175
Diffstat (limited to 'toplevel')
0 files changed, 0 insertions, 0 deletions