Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] PG: quirk in proof faces configuration

view this post on Zulip Email Gateway (Aug 18 2022 at 17:39):

From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi,

trying to change the color of string delimiters in PG/Isabelle, I
observed that the
starting quote of a string is bound to "Isabelle Quote Face". However,
the final quote of a string is bound to "Proof Boring Face".
The second binding is counter-intuitive and does not match the
description of "Proof Boring Face".

I'm using the PG Version 4.1pre101216 on GNU Emacs 23.2.1 (The
PG-Version that ships with Isabelle2011 by default)

Best,
Peter

p.s. If this is an issue for the ProofGeneral developers, where to post it?

view this post on Zulip Email Gateway (Aug 18 2022 at 17:40):

From: David Aspinall <David.Aspinall@ed.ac.uk>

starting quote of a string is bound to "Isabelle Quote Face". However,
the final quote of a string is bound to "Proof Boring Face".

I've fixed this no in PG CVS, thanks for the correction.

p.s. If this is an issue for the ProofGeneral developers, where to post it?

Please use http://proofgeneral.inf.ed.ac.uk/trac/

(registration disabled, login as "isabelleuser" password "isabelle")

- David

Last updated: Apr 25 2024 at 20:15 UTC