Attempt to fix filename mess for Windows.

2 files changed, 21 insertions, 2 deletions

diff --git a/isa/isa.el b/isa/isa.el
index 01121a80..aa5bad34 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -145,8 +145,18 @@ and script mode."
    proof-shell-cd-cmd			"Library.cd \"%s\""
 
    ;; Escapes for filenames inside ML strings.
+   ;; We also make a hack for a bug in Isabelle, by switching from 
+   ;; backslashes to forward slashes if it looks like we're running
+   ;; on Windows.
    proof-shell-filename-escapes		
-   '(("\\\\" . "\\\\") ("\""   . "\\\""))
+   (if (fboundp 'win32-long-filename)	; rough test for XEmacs on win32 
+       ;; Patterns to unixfy names.
+       ;; Jacques Fleuriot's patch in ML does this too: ("^[a-zA-Z]:" . "") 
+       ;; But I'll risk leaving drive names in, not sure how to replace them.
+       '(("\\\\" . "/") ("\"" . "\\\""))
+     ;; Normal case: quotation for backslash, quote mark.
+     '(("\\\\" . "\\\\") ("\""   . "\\\"")))
+
 
    ;; FIXME: the next two are probably only good for NJ/SML
    proof-shell-interrupt-regexp         "Interrupt"
diff --git a/isar/isar.el b/isar/isar.el
index 866bee75..30a174cd 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -245,8 +245,17 @@
    proof-shell-cd-cmd			"ML {* Library.cd \"%s\" *}"
 
    ;; Escapes for filenames inside ML strings.
+   ;; We also make a hack for a bug in Isabelle, by switching from 
+   ;; backslashes to forward slashes if it looks like we're running
+   ;; on Windows.
    proof-shell-filename-escapes		
-   '(("\\\\" . "\\\\") ("\""   . "\\\""))
+   (if (fboundp 'win32-long-filename)	; rough test for XEmacs on win32 
+       ;; Patterns to unixfy names.
+       ;; Jacques Fleuriot's patch in ML does this too: ("^[a-zA-Z]:" . "") 
+       ;; But I'll risk leaving drive names in, not sure how to replace them.
+       '(("\\\\" . "/") ("\"" . "\\\""))
+     ;; Normal case: quotation for backslash, quote mark.
+     '(("\\\\" . "\\\\") ("\""   . "\\\"")))
 
    proof-shell-proof-completed-regexp   nil     ; n.a.
    proof-shell-interrupt-regexp         "\364\\*\\*\\* Interrupt\\|\360Interrupt"