--- 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%
-
-<p><a href="http://www.apple.com/macosx/">Mac OS X</a> is the current version
-of the Macintosh operating system, installed on all new <a href=
-"http://www.apple.com/">Apple</a> computers. Because it is based on Unix, it
-can run <a href=
-"http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">Isabelle</a>. The new
-<a href="http://www.apple.com/powermac/">Power Mac G5</a> is an excellent
-Isabelle machine. Here is a <a href="isabelle_macos_screenshot.jpg">screenshot</a>
-showing Proof General running in GNU Emacs.</p>
-
-<p>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.</p>
-
-<ol>
-<li>Download Isabelle to a suitable directory, as described on the
-<a href="packages.html">download page</a>. Be sure to get the following files
-
-<ul>
-<li><tt><!-- _GP_ href(distname . ".tar.gz", distname . ".tar.gz") --></tt></li>
-<li><tt><!-- _GP_ href("contrib/ProofGeneral.tar.gz", "ProofGeneral.tar.gz") --></tt></li>
-<li><tt><!-- _GP_ href("contrib/polyml_base.tar.gz", "polyml_base.tar.gz") --></tt></li>
-<li><tt><!-- _GP_ href("contrib/polyml_ppc-darwin.tar.gz", "polyml_ppc-darwin.tar.gz") --></tt></li>
-<li><tt><!-- _GP_ href("HOL_ppc-darwin.tar.gz", "HOL_ppc-darwin.tar.gz") --></tt></li>
-</ul>
-</li>
-
-<li>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 <a href=
-"http://fink.sourceforge.net/">Fink</a>.</li>
-
-<li>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
-<tt>Isabelle/INSTALL.</tt></li>
-
-<li>You should also be able to launch <a
-href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a> by typing
-"<tt>Isabelle</tt>" 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 <a href=
-"http://home.att.ne.jp/alpha/z123/emacs-mac-e.html">MacEmacs JP</a> or
-<a href="http://mindlube.com/products/emacs/">mindlube's</a> or <a
-href= "http://www.cs.man.ac.uk/%7efranconi/mac-emacs/">Enhanced Carbon
-Emacs</a>. Visiting a theory file from Emacs will automatically
-launch Proof General provided <tt>isabelle</tt> is on the search
-path. None of these options support the X-Symbol package,
-unfortunately.</li> </ol>
-
-<p>In order to get the full benefit of Proof General, you must install the X
-Window System (X11) and <a href="http://www.xemacs.org/">XEmacs</a> or
-<a href="http://www.gnu.org/software/emacs/emacs.html">GNU Emacs</a>.</p>
-
-<ul>
-<li><a href="http://www.apple.com/macosx/x11/">Apple's version</a> 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.</li>
-
-<li>Some people prefer the <a href=
-"http://www.osxgnu.org/software/Xwin/WindowManagers/OroborOSX/">OroborOSX</a>
-window manager. It must be used in conjunction with <a href=
-"http://xfree86.org/">XFree86</a>, which is easy to install if you use the
-installer provided by the <a href=
-"http://sourceforge.net/projects/xonx/">XonX</a> project.</li>
-</ul>
-
-<p>The easiest way to install XEmacs or GNU Emacs is via the package manager
-<a href="http://fink.sourceforge.net/">Fink</a>. Install the Fink package
-<tt>xemacs-sumo-pkg</tt> to get the XEmacs libraries that Proof General needs
-to run. To install GNU Emacs, install the package <tt>emacs21</tt>. Fink can
-compile from sources, but this takes hours, so it is better to request binary
-installations.</p>
-
-<p>To use <a href="http://www.gnu.org/software/emacs/emacs.html">GNU
-Emacs</a> instead of <a href="http://www.xemacs.org/">XEmacs</a>, you must
-recompile Proof General and X-Symbol following the instructions <a href=
-"http://proofgeneral.inf.ed.ac.uk/FAQ">here</a>. Note that Proof General
-incorporates its own copy of X-Symbol.</p>
-
-<ol>
-<li>Install X11 or OroborOSX.</li>
-
-<li>Install XEmacs (and its libraries), or install GNU Emacs and recompile
-Proof General.</li>
-
-<li>You may want to install this drag-and-drop <a href=
-"IsabelleDroplet.dmg">Isabelle launcher</a>. It is a simple hack that
-invokes xemacs on any files dropped on it.</li>
-</ol>
-