I've had what I consider to be success with a very similar setup...
I'm using:
Isabelle (isa2011-test1: January 2011, which has Proof General Version
4.1pre110112)
but with Aquamacs Distribution 2.1
on MacOS 10.6
I'm loading Aquamacs from the dock, so I don't get background noise.
Menus respond with usual swiftness and long arrows/unicode tokens etc
look good.
Setup .emacs config:
(custom-set-variables
'(isa-isabelle-command "/Applications/isa2011-test1.app/Isabelle
/bin/isabelle"))
(load-file
"/Applications/isa2011-test1.app/Isabelle/contrib/ProofGeneral/generic/proof-site.el")
Light blue background looks just right on my screen/default setup.
I wasn't able to reproduce the syntax-highlighting bug.
best,
lucas
On 23/01/2011 18:57, Clemens Ballarin wrote:
I repeated my recent try of ProofGeneral on my Mac with
ProofGeneral-4.1pre110118. If used with Aquamacs I observe these issues:
- Menus respond slowly (> 1 second) when invoked for the first time.
This is fine if Aquamacs is used without ProofGeneral.
- Noise on the background shell.
- Fontification fails in one situation. See attached image.
- Long arrows are displayed as boxes (I probably don't have a suitable
font for this.)
- Light blue background of processed portion of the buffer is hard to see.
Unicode symbols that are available are displayed in the right size. This
is much better than with my previous setup with PG 3.7.1.1 and Carbonemacs.
If the slow menus can be fixed this might be a suitable companion for
Isabelle 2011.
Clemens
PS. I did use this configuration:
- Aquamacs 2.1 distribution
- ProofGeneral-4.1pre110118
- MacOS X 10.5.8
Quoting Makarius <[email protected]>:
On Fri, 21 Jan 2011, Mamoun FILALI-AMINE wrote:
a remark: previously, there was aquamacs instead of emacs? I find
auqamacs more convenient than emacs.
In recent Isabelle releases the default combination was Proof General
3.7.1.1 with Aquamacs based on Emacs 22. That turned out as
half-decent, half-working -- after many weeks of desparate search in
the Mac OS X ecosphere.
In Isabelle2011 the default Proof General is going to be 4.1, which
has quite different Emacs requirements, and generally quite different
behaviour concerning special symbols etc.
So far, I did not spend much time to try all possible combinations of
Emacsen with PG 4.1. According to ProofGeneral/COMPATIBILITY, plain
GNU Emacs 23.2 is recommended (aka the "no nonsense version").
Aquamacs 2.1 is also based on that code base, so it could in principle
work as well, despite fancy additions.
When I've tried the slightly older Aquamacs 2.0 some months ago, it
turned out much slower than plain GNU Emacs 23 -- see also
http://proofgeneral.inf.ed.ac.uk/trac/ticket/324 -- but that might be
obsolete in several respects.
I hope to get more concrete feedback from Mac users. So far I've
mainly found out that most people are stuck with very old versions of
Proof General, sometimes even in combination with ancient XEmacs.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
