aboutsummaryrefslogtreecommitdiff
path: root/isar
diff options
context:
space:
mode:
authorDavid Aspinall2000-03-24 09:57:46 +0000
committerDavid Aspinall2000-03-24 09:57:46 +0000
commit8f40ffb2b100ab2fa8455f30322d700895cd740b (patch)
treedd091526f4be6ceb673299b679ae1c3311f72946 /isar
parent4c4d187ab372d7433a7a80eb9aa521f9bb9db4e0 (diff)
Attempt to fix filename mess for Windows.
Diffstat (limited to 'isar')
-rw-r--r--isar/isar.el11
1 files changed, 10 insertions, 1 deletions
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"