added ML antiquotation @{make_string}, which produces proper pretty printed version in Poly/ML 5.3.0 or later;
Some notes on platform support of Isabelle
==========================================
Preamble
--------
The general programming model is that of a stylized ML + Scala + POSIX
environment, with hardly any system specific code in user-space tools
and packages.
The basic Isabelle system infrastructure provides some facilities to
make this work, e.g. see the ML structures File and Path, or functions
like bash_output. The settings environment also provides some means
for portability, e.g. jvm_path to hold up the impression that even
Java on Windows/Cygwin adheres to Isabelle/POSIX standards.
When producing add-on tools, it is important to stay within this clean
room of Isabelle, and refrain from overly ambitious system hacking.
Supported platforms
-------------------
The following hardware and operating system platforms are officially
supported by the Isabelle distribution (and bundled tools):
x86-linux
x86-darwin
x86-cygwin
x86_64-linux
x86_64-darwin
As of Cygwin 1.7 there is only a 32 bit version of that platform. The
other 64 bit platforms become more and more important for power users
and always need to be taken into account when testing tools.
All of the above platforms are 100% supported -- end-users should not
have to care about the differences at all. There are also some
secondary platforms where Poly/ML also happens to work:
ppc-darwin
sparc-solaris
x86-solaris
x86-bsd
There is no guarantee that Isabelle add-ons work on these fringe
platforms. Even Isabelle/Scala already fails on ppc-darwin due to
lack of JVM 1.6 support on that platform.
Dependable system tools
-----------------------
The following portable system tools can be taken for granted:
* GNU bash as uniform shell on all platforms. Note that the POSIX
"standard" shell /bin/sh is *not* appropriate, because there are
too many different implementations of it.
* Perl as largely portable system programming language. In some
situations Python may as an alternative, but it usually performs
not as well in addressing various delicate details of basic
operating system concepts (processes, signals, sockets etc.).
* Scala with Java Runtime 1.6. The Isabelle/Pure.jar library irons
out many oddities and portability problems of the Java platform.
Known problems
--------------
* Mac OS: If MacPorts is installed and its version of Perl takes
precedence over /usr/bin/perl in the PATH, then the end-user needs
to take care of installing add-on modules, e.g. HTTP support. Such
add-ons are usually included in Apple's /usr/bin/perl by default.
* The Java runtime has its own idea about the underlying platform,
e.g. on 64 bit machine Isabelle/ML could be x86-linux, but the JVM
could be x86_64-linux. This affects Java native libraries in
particular -- which are very hard to support in a platform
independent manner, and should be avoided in the first place.