MacOS X Emacs hints
+ +Assuming you have an installation of Isabelle on your Mac, + there are various possibilites for running ProofGeneral:
+ +-
+
- You should also be able to launch Proof General by typing + Isabelle at the Unix command line. This will invoke the + Apple-supplied version of Emacs in a terminal window, providing a primitive + environment. +
- Somewhat better is to run Proof General from within a version + of Emacs ported as a native Mac OS X application, such as MacEmacs JP or + mindlube's or Enhanced Carbon Emacs. + Visiting a theory file from Emacs will automatically launch Proof General + provided isabelle is on the search path. None of these options + support the X-Symbol package, unfortunately. +
- In order to get the full benefit of Proof General, you must install the X + Window System (X11) and XEmacs or + GNU Emacs. +
- + apple's version of X11 + is included with the Panther (MacOS X 10.3) installation discs, though it is + not installed by default. The Command key serves as Meta, but it is + reserved for standard Apple shortcuts such as C, V and X, so you must use + Esc-C, Esc-V and Esc-X in Emacs or else deselect »Enable key equivalents« + in the X11 preferences. +
- The easiest way to install XEmacs or GNU Emacs is via the package manager + Fink. Install the Fink package + xemacs-sumo-pkg to get the XEmacs libraries that Proof General needs + to run. To install GNU Emacs, install the package emacs21. Fink can + compile from sources, but this takes hours, so it is better to request binary + installations. +
- To use GNU + Emacs instead of XEmacs, you must + recompile Proof General and X-Symbol following the instructions here. Note that Proof General + incorporates its own copy of X-Symbol. + +
-
+
You may want to install this drag-and-drop Isabelle launcher. It is a simple hack that + invokes XEmacs on any files dropped on it.
+ +Here is a screenshot showing Proof General running + in GNU Emacs.
+ +