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.

Thank you!

Rafal Kolanski.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.