aboutsummaryrefslogtreecommitdiff
path: root/isa
diff options
context:
space:
mode:
Diffstat (limited to 'isa')
-rw-r--r--isa/isa.el12
1 files changed, 11 insertions, 1 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"