[isabelle-dev] Proof General 4.1 on Mac OS X

[Clemens Ballarin]

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



-------------- next part --------------
A non-text attachment was scrubbed...
Name: Picture 1.png
Type: image/png
Size: 24097 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110123/e3727382/attachment-0002.png>