Re: [isabelle] Does anyone know how to get rid of => marker in PG4.0?
David Aspinall wrote:
I confirmed this fix works, but would like to add I'm not using emacs
in tty mode, it's the GTK+ version with unicode fonts and Xft working
as comes in ubuntu-snapshot with ubuntu 9.10. I don't have any
"gutter" to the left of my text though, so that may be the problem. As
for a triangle vs "=>", I honestly have no idea.
Is there some reason you need the emacs-snapshot rather than the stable
emacs23 package? I've tried emacs23 and it displays the gutter
properly. Latest update also has the GTK fix.
I only run the emacs-snapshot because I needed it to get emacs 23 on
Ubuntu 9.04 and upgraded into it. I don't need to keep running the
snapshot, but at the moment the two versions are nearly identical anyway.
In this case I just had the gutter turned off, probably using:
"(fringe-mode 0 nil (fringe))". By this I assumed everything that
appears in the gutter (such as line numbers, the "=>" marker or
triangle) would simply not appear. I did not consider that it would
appear in the window, overlaying normal text instead.
I have no wish to point fingers at emacs or proof general, I just needed
an emacs/PG guru to shake the aforementioned assumption out of me (I am
not an emacs guru, not even intermediate, I only ever use it for Isabelle).
David did this, his fix works, and the next time someone turns off the
gutter to maximise horizontal space usage (e.g. two proof generals side
by side), they will have something to search for :)
Am I OK to conclude from this exchange that emacs 23.1 is to be
considered "blessed"? Trying to get the versioning of the
PolyML/Isabelle/PG/Emacs combo right is sometimes... interesting.
This archive was generated by a fusion of
Pipermail (Mailman edition) and