Email Gateway (Aug 18 2022 at 17:32): Email Gateway (Aug 18 2022 at 17:32):From: Christoph Sprenger <sprenger@inf.ethz.ch>
Hi,
I have recently installed the Isabelle 2011 on Mac Application, which
includes
Carbon Emacs 23.2, and
ProofGeneral 4.1pre101216
(before I was using Isabelle 2009-1 with CE 22.3 and PG 3.7.1.1).
There a number of "features" of this combo that tend to drive me nuts.
These are:
1) The Emacs Meta modifier is bound to the Option key instead of the
Command key.
2) The Delete key acts like Backspace.
3) When I point the mouse on a processed part of the input it becomes
highlighted in yellow and displays a "tooltip" frame with info about
the underlying object. Inside proofs it shows the proof state at the
mouse position. While this looks like a cool new feature in PG4, I
would like to be able to turn both the highlighting and the "tooltips"
off, when I do not need them. However, I was unable to find an option
that achieves this.
4) There seem to be some bugs in PG 4 by which
the command processing gets out of sync (previously rare), indicated
by the highlighting ending in the middle of a syntactic token or input
sentence,
the highlighting is not properly removed and some bits of processed
input stay yellow, after the mouse is moved away.
1) and 2) seem to be PG-independent "features" of CE 23.2 (does my CE
22 config possibly disturb CE 23?), while 3) and 4) are PG-specific.
Point 4) is less of a problem than the others, since it does not occur
very often.
I would greatly appreciate any help with these issues.
Best wishes,
Christoph
Email Gateway (Aug 18 2022 at 17:33):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Christoph,
I would greatly appreciate any help with these issues.
I ran into much the same issues, plus some more, including
5) Windows that appear to prompt the user (e.g., "Do you want to save?") sometimes had absolutely ridiculous geometries, like 1000000 pixels wide. They were so wide that all I saw was a gray panel in the middle of the screen, which I couldn't close (the close button was like 500000 pixels to the left of the screen). I had to kill the app. This happened often enough to make the application totally unusable.
This convinced me very quickly to go back to the "good old" Aquamacs. Not that I'm a big fan of the beast, but at least I know its bugs and I'm used to work around them.
In my .bashrc file, I have the lines
export EMACS=/Applications/Isabelle2009-2.app/Contents/Resources/Emacs.app/Contents/MacOS/Emacs
alias Isabelle="/Applications/Isabelle2011.app/Isabelle/bin/isabelle emacs -p $EMACS"
Then I can launch Isabelle2011 with the Aquamacs from Isabelle2009-2 by entering "Isabelle" on the command line.
Jasmin
Email Gateway (Aug 18 2022 at 17:33):From: Brian Huffman <brianh@cs.pdx.edu>
On Tue, Apr 12, 2011 at 5:38 AM, Christoph Sprenger
<sprenger@inf.ethz.ch> wrote:
Hi,
I have recently installed the Isabelle 2011 on Mac Application, which
includesCarbon Emacs 23.2, and
ProofGeneral 4.1pre101216
[...]
2) The Delete key acts like Backspace.
This one at least is not too hard to fix. You will need to customize
the option "normal-erase-is-backspace", which you can do using
Options > Customize Emacs > Specific Option...
and typing in "normal-erase-is-backspace". Try setting the value to
"On", and see if this solves your problem.
I also have a related-but-different problem with delete vs. backspace
in the same version of ProofGeneral, but on Linux (Ubuntu) with GNU
Emacs 23.2.1. The delete key normally works properly, doing
forward-delete; but the symbol input shortcuts cause problems. For
example, if I have just typed "-" or "--" (which are prefixes of
"-->", the shortcut for the \<longrightarrow> symbol), then my
"delete" key works like "backspace" instead.
Interestingly, Carbon Emacs seems to do the right thing in this
situation once I have "normal-erase-is-backspace" set properly, but
GNU Emacs on Linux gets it wrong no matter how
"normal-erase-is-backspace" is set.
3) When I point the mouse on a processed part of the input it becomes
highlighted in yellow and displays a "tooltip" frame with info about the
underlying object. Inside proofs it shows the proof state at the mouse
position. While this looks like a cool new feature in PG4, I would like to
be able to turn both the highlighting and the "tooltips" off, when I do not
need them. However, I was unable to find an option that achieves this.
I would also like to be able to turn this feature off.
Email Gateway (Aug 18 2022 at 17:33):From: David Aspinall <David.Aspinall@ed.ac.uk>
http://tinyurl.com/pgchap3
Email Gateway (Aug 18 2022 at 17:33):From: David Aspinall <David.Aspinall@ed.ac.uk>
4) There seem to be some bugs in PG 4 by which
- the command processing gets out of sync (previously rare), indicated by the highlighting ending in the middle of a syntactic token or input sentence,
If you can repeat this, please report the bug at http://proofgeneral.inf.ed.ac.uk/trac
- the highlighting is not properly removed and some bits of processed input stay yellow, after the mouse is moved away.
Sounds likely to be a Emacs display engine bug rather than PG. Try searching/reporting at
http://debbugs.gnu.org/
Email Gateway (Aug 18 2022 at 17:33):From: Alexander Krauss <krauss@in.tum.de>
This didn't help me. As I understand it, switching off "Full Annotation"
should prevent saving (and displaying) the prover output. But even when
disabled, I still get the tooltips, and they normally sit right in front
of the text I am trying to read, forcing me to move the mouse.
As a workaround, I discovered that turning off "tooltip-mode" removes
the gigantic tooltips and instead displays the text in the minibuffer,
which is less intrusive.
The yellow highlight can be removed by customizing the appropriate face.
Unfortunately, the syntax highlighting of the normal text (foreground
colour) still disappears on mouseover...
Alex
Email Gateway (Aug 18 2022 at 17:33):From: David Aspinall <David.Aspinall@ed.ac.uk>
This didn't help me. As I understand it, switching off "Full Annotation" should prevent saving (and displaying) the prover output. But even when disabled, I still get the tooltips, and they normally sit right in front of the text I am trying to read, forcing me to move the mouse.
I see your point -- when "full annotation" is switched off, they're only added for incrementally processed steps and won't be removed from already processed portions of the script. It might be better to have an option to prevent adding them altogether.
As a workaround, I discovered that turning off "tooltip-mode" removes the gigantic tooltips and instead displays the text in the minibuffer, which is less intrusive.
You can also customize tooltip-delay and tooltip-short-delay.
Or use your finger to point at what you're reading, 8-).
The yellow highlight can be removed by customizing the appropriate face. Unfortunately, the syntax highlighting of the normal text (foreground colour) still disappears on mouseover...
This is by poor/old design in the Emacs display engine, which replaces (rather than merges) the mouse-over face with the underlying one which doesn't work well with font lock. You see the same thing in Emacs native modes, e.g. Info. I reported it as an Emacs bug a while ago.
Email Gateway (Aug 18 2022 at 17:33):From: Makarius <makarius@sketis.net>
I have something like this in my
$ISABELLE_HOME_USER/etc/proofgeneral-settings.el, but you can also use the
customization menu in Emacs:
(setq mac-option-modifier nil)
Makarius
Email Gateway (Aug 18 2022 at 17:33):From: Christoph Sprenger <sprenger@inf.ethz.ch>
Dear Brian and Makarius,
thank you for your helpful suggestions regarding the Emacs-specific
problems 1) and 2).
@Brian regarding backspace problem:
Setting normal-erase-is-backspace to On solves my problem.
@Makarius regarding modifier keys:
Your command switches off the interpretation of the Option key by
Emacs, which is good. But I also and had to set mac-command-modifier
to meta in order to restore things to "normal". I did this via the
menus, so my .emacs now contains
(custom-set-variables
...
'(ns-alternate-modifier (quote none))
'(ns-command-modifier (quote meta))
...
)
Here, ... denotes other settings and "ns-command-modifier" is a
synonym for "mac-command-modifier" and similarly for the other.
Best,
Christoph
Email Gateway (Aug 18 2022 at 17:33):From: Christoph Sprenger <sprenger@inf.ethz.ch>
This didn't help me. As I understand it, switching off "Full
Annotation" should prevent saving (and displaying) the prover
output. But even when disabled, I still get the tooltips, and they
normally sit right in front of the text I am trying to read,
forcing me to move the mouse.I see your point -- when "full annotation" is switched off, they're
only added for incrementally processed steps and won't be removed
from already processed portions of the script. It might be better
to have an option to prevent adding them altogether.
Exactly.
As a workaround, I discovered that turning off "tooltip-mode"
removes the gigantic tooltips and instead displays the text in the
minibuffer, which is less intrusive.You can also customize tooltip-delay and tooltip-short-delay.
Or use your finger to point at what you're reading, 8-).
I have set these two variables to a longer delay (5s) for now, which
helps.
The yellow highlight can be removed by customizing the appropriate
face. Unfortunately, the syntax highlighting of the normal text
(foreground colour) still disappears on mouseover...This is by poor/old design in the Emacs display engine, which
replaces (rather than merges) the mouse-over face with the
underlying one which doesn't work well with font lock. You see the
same thing in Emacs native modes, e.g. Info. I reported it as an
Emacs bug a while ago.
I have currently set the following variables
proof-command-mouse-highlight-face
proof-mouse-highlight-face
proof-region-mouse-highlight-face
to the same color (lightblue in my case) as
proof-locked-face
In this way, the previous MTV-style flickering while moving the mouse
is reduced to the disappearing syntax highlighting, which I find less
distracting.
Thank you all for your helpful hints.
Best,
Christoph
Last updated: Nov 21 2024 at 12:39 UTC