diff -r f9f2e1643593 -r 322e2a3335d4 Admin/page/dist-content/notes_macos_darwin.content
--- a/Admin/page/dist-content/notes_macos_darwin.content Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,100 +0,0 @@
-%title%
-Isabelle under Mac OS X
-
-%body%
-
-Mac OS X is the current version
-of the Macintosh operating system, installed on all new Apple computers. Because it is based on Unix, it
-can run Isabelle. The new
-Power Mac G5 is an excellent
-Isabelle machine. Here is a screenshot
-showing Proof General running in GNU Emacs.
-
-This page gives advice on building Isabelle for Mac OS X. It assumes that
-you are familiar with both Mac OS X and Unix. You must have installed the Mac
-OS X developer tools.
-
-
-- Download Isabelle to a suitable directory, as described on the
-download page. Be sure to get the following files
-
-
-
-
-- You may have to install the bash shell. Versions of Mac OS X prior to
-10.2.2 did not provide it. If /bin/bash does not exist, you can install it
-using the package manager Fink.
-
-- At this point, you should be able to run Isabelle with the command line
-interface. You can also build Isabelle from the Unix command line,
-following the instructions for "Compiling Logics" in file
-Isabelle/INSTALL.
-
-- 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 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.
-
-- Some people prefer the OroborOSX
-window manager. It must be used in conjunction with XFree86, which is easy to install if you use the
-installer provided by the XonX project.
-
-
-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.
-
-
-- Install X11 or OroborOSX.
-
-- Install XEmacs (and its libraries), or install GNU Emacs and recompile
-Proof General.
-
-- 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.
-
-
