[isabelle-dev] Isabelle_11-Sep-2011

Makarius makarius at sketis.net
Fri Sep 30 17:37:41 CEST 2011


On Fri, 30 Sep 2011, Bertram Felgenhauer wrote:

> Dear Makarius and René,
>
>>> However, testing Isabelle_20-Sep-2011 with Emacs 23.3, there seems to be a problem for Mac OS Lion users:
>>> Many special characters like ==> \in, => are not displayed correctly which makes working inconvenient. Under
>>>
>>> http://cl-informatik.uibk.ac.at/~thiemann/emacs.html
>
> I believe I know this bug. It's an emacs problem, and should be fixed in 
> emacs 23.4 once it becomes available. That said I don't know of any 
> elisp code other than ProofGeneral that tickles this bug. As far as 
> Isabell/PG are concerned, it's not a new problem -- it also affects 
> Isabelle2011. See
>
>  http://debbugs.gnu.org/cgi/bugreport.cgi?bug=8703
>
> (Note that I encountered this problem with Linux -- I hope that the 
> MacOS version uses the same code, but I have not tested this theory.)

What is odd about it: with the same Emacs-23.2.1 on Mac OS X the problem 
only occurs on Lion, not Snow Leopard (which I have started to re-install 
today on my desktop system).

Since Emacs-23.2.1 has only a *few* such drop-outs on Lion, but Emacs-23.3 
has *many*, I have switched back to the older version in the app bundle on 
http://isabelle.in.tum.de/website-Isabelle2011-1-RC1/


 	Makarius


More information about the isabelle-dev mailing list