[isabelle] Running cygwin isabelle from windows Gnu Emacs


I'm trying to run the cygwin version of isabelle from my Windows Gnu Emacs
22.1.  I successfully built isabelle from the cygwin-x86 image, calling
"build" to compile HOL.  When I call "isabelle" from a cygwin bash window, I

> val it = () : unit
val commit = fn : unit -> bool

which I'm assuming is right.

I have set isabelle-program-name to point to a batch file that sits in the
emacs bin directory.  The latest version of the batch file says:

rem @echo off
rem set ISATOP=/usr/local/Isabelle2007
rem set ISALIB=%ISATOP%/lib
set ISABINWINDOWS=C:\Cygwin\usr\local\Isabelle2007\bin
rem set ISABIN=%ISATOP%/bin
rem set PATH=%PATH%;%ISABIN%
bash %ISABINWINDOWS%\isabelle-process %1 %2 %3

(This is based on a working script to call coq from proof general).

When I do this, I get the following in the *response* buffer:

*** Exception-
***    ERROR "Illegal character(s) \":\" in path element specification:
***    raised
*** At command "ML_command".

It looks like I'm actually reaching some part of the isabelle system, but
something is finding a Windows path when it's looking for a cygwin path.

Anybody have any guesses as to what this might be?

--Mitch Wand

PS: Yes, I've tried running isabelle-interface-- this pops up a Gnu Emacs
under X and starts Proof General, but I get File mode specification error:
(file-error "Searching for program" "no such file or directory"
"C:\\cygwin\\bin\\tcsh.exe") .  Since I use my native Windows emacs for
everything else, I'd like to pursue that line first.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.