On Mon, 19 May 2014, David Matthews wrote:
Using Cygwin might be a possibility if you are thinking of providing a separate GUI. The package that Makarius has provided for running Isabelle on Windows uses Poly/ML under Cygwin but all the user interaction is through jEdit.
Isabelle/jEdit is merely the front-end. The actual connectivity happens via Isabelle/Scala, which is just a JVM plus some Scala-implemented jars. All the system plumbing is done via the Java APIs, which might sound odd, since Java traditionally achieves platform-indepence by omitting important platform-specific operations (e.g. POSIX kill), but in Java 7 it has greatly improved.
The JVM process could be replaced by some more native Windows program, but we depend on the JVM anyway, so it is the canonical solution.
There are also some funny add-on scripts, e.g. to make a named pipe on Unix, but on Windows we are using regular TCP sockets to connect the ML process.
There might be issues, though, if you wanted the ML code to access the Windows filing system because Cygwin imposes its own view of the filing system.
Here we merely use POSIX-ish notation, e.g. /cygdrive/c instead of C:\ The Isabelle/Scala library has operations to convert between different formats, and gives the ML process what it expects. This also works for Windows network paths //server/share/foo/bar -- better than TeXlive on that platform.
The jEdit editor has its own traditions to iron out Windows vs. POSIX differences, such that users of Isabelle/jEdit can refer to things like $ISABELLE_HOME/src/HOL/HOL.thy literally in that Isabelle-specific notation, just by coincidence.
Makarius