Re: [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
> get
> 

I'm using the same combination for several years with a personally patched
version of Isabelle. It might also work for you. 

The code below just converts a Windows path into a cygwin path by calling
"cygpath" command of cygwin. 

Yasuhiko Minamide


diff -cr Isabelle_08-May-2007/src/Pure/General/path.ML Isabelle_08-May-2007-windows/src/Pure/General/path.ML
*** Isabelle_08-May-2007/src/Pure/General/path.ML	Fri Dec 15 08:08:09 2006
--- Isabelle_08-May-2007-windows/src/Pure/General/path.ML	Wed May  9 10:40:14 2007
***************
*** 120,129 ****
  
  val explode_elems = map explode_elem o filter_out (fn c => c = "" orelse c = ".");
  
! fun explode_path str = Path (norm
    (case space_explode "/" str of
      "" :: ss => Root :: explode_elems ss
!   | ss => explode_elems ss));
  
  
  (* base element *)
--- 120,138 ----
  
  val explode_elems = map explode_elem o filter_out (fn c => c = "" orelse c = ".");
  
! (* fun explode_path str = Path (norm
    (case space_explode "/" str of
      "" :: ss => Root :: explode_elems ss
!   | ss => explode_elems ss)); *)
! 
! fun explode_path str = 
!   let val str = execute ("cygpath "^str) 
!       val str = String.substring (str, 0, String.size str - 1) in
!   Path (norm
! 	  (case space_explode "/" str of
! 	    "" :: ss => Root :: explode_elems ss
!             | ss => explode_elems ss))
!   end;
  
  
  (* base element *)






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