Re: [isabelle] Does anyone know how to get rid of => marker in PG4.0?

David Aspinall wrote:

=>mma "1 + 1 = 2" oops

I've also seen this marker, but only as a small graphical triangle left of the text area. (This was something like GNU Emacs 23.1.1.)

I replied off list to Rafal as I didn't try the fix:

(setq overlay-arrow-string "")

This marker is shown as text in tty mode when the graphical triangle isn't available. It has the same overwriting behaviour where it's used in other Emacs modes (e.g., edebug). The arrow doesn't get in the way when the text is indented beyond the first column.

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.


Rafal Kolanski.

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