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 <makar...@sketis.net>:

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
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




<<attachment: Picture 1.png>>

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to