Re: [isabelle] Getting Isabelle Running with Xemacs



Larry didn't mention his useful page on getting Isabelle and Proof General running on Macs, here:

  http://www.cl.cam.ac.uk/research/hvg/Isabelle/macosx.html

I stole the PG part of this and put it onto the Proof General Wiki:

  http://proofgeneral.inf.ed.ac.uk/wiki/Main/PGEmacsOnMacOSX

I've added a bit more about native Emacs ports: I've been using Carbon Emacs for a while, it works pretty well and looks pretty (antialised fonts!). The main problem for Isabelle is the lack of X- Symbol, but actually I don't think this is *too* difficult to fix. A while ago I had a try, and I've put some notes now onto the Wiki which describe what I did:

  http://proofgeneral.inf.ed.ac.uk/wiki/Main/XSymbolOnMacOSX

Someone who has a bit of time (and a penchant for font formats) could get things working along any of the three lines I describe. The second and third solutions would not be just for Mac: Carbon Emacs is based on the future Unicode based version of GNU Emacs which supports rendering using Xft. It seems to work reasonably reliably on Linux, but you have to build it yourself from CVS.

  - David.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.