aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall2000-03-22 13:03:48 +0000
committerDavid Aspinall2000-03-22 13:03:48 +0000
commit8c14c8e72ff6e093f0a35c56f8982ba2a3b2785c (patch)
tree7690e348d61df39524d0f070c515841a0c30df77
parent04dae31678bbb6eb58e957a88625de44da1fa97c (diff)
Fix other file commands to use %e substitution.
-rw-r--r--isa/isa.el16
-rw-r--r--isar/isar.el4
2 files changed, 11 insertions, 9 deletions
diff --git a/isa/isa.el b/isa/isa.el
index 54d40621..1945f0d3 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -125,9 +125,9 @@ and script mode."
proof-shell-compute-new-files-list 'isa-shell-compute-new-files-list
proof-shell-inform-file-processed-cmd
- "ProofGeneral.inform_file_processed \"%s\";"
+ "ProofGeneral.inform_file_processed \"%e\";"
proof-shell-inform-file-retracted-cmd
- "ProofGeneral.inform_file_retracted \"%s\";"))
+ "ProofGeneral.inform_file_retracted \"%e\";"))
(defun isa-shell-mode-config-set-variables ()
@@ -250,8 +250,9 @@ and script mode."
(defun isa-update-thy-only (file try wait)
"Tell Isabelle to update current buffer's theory, and all ancestors."
(proof-shell-invisible-command
- (format "ProofGeneral.%supdate_thy_only \"%s\";"
- (if try "try_" "") (file-name-sans-extension file))
+ (proof-format-filename
+ (format "ProofGeneral.%supdate_thy_only \"%%e\";" (if try "try_" ""))
+ (file-name-sans-extension file))
wait))
(defun isa-shell-update-thy ()
@@ -379,7 +380,7 @@ isa-proofscript-mode."
(save-some-buffers)
(isa-update-thy-only file nil nil))
-(defcustom isa-retract-thy-file-command "ThyInfo.remove_thy \"%s\";"
+(defcustom isa-retract-thy-file-command "ThyInfo.remove_thy \"%e\";"
"Sent to Isabelle to forget theory file and descendants.
Resulting output from Isabelle will be parsed by Proof General."
:type 'string
@@ -393,8 +394,9 @@ you will be asked to retract the file or process the remainder of it."
(interactive (list buffer-file-name))
(proof-deactivate-scripting)
(proof-shell-invisible-command
- (format isa-retract-thy-file-command
- (file-name-nondirectory (file-name-sans-extension file)))))
+ (proof-format-filename isa-retract-thy-file-command
+ (file-name-nondirectory
+ (file-name-sans-extension file)))))
;; Next bits taken from isa-load.el
diff --git a/isar/isar.el b/isar/isar.el
index 9914c7b8..f65b78cd 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -299,8 +299,8 @@
proof-shell-retract-files-regexp
"Proof General, you can unlock the file \"\\(.*\\)\""
proof-shell-compute-new-files-list 'isar-shell-compute-new-files-list
- proof-shell-inform-file-processed-cmd "ProofGeneral.inform_file_processed \"%s\";"
- proof-shell-inform-file-retracted-cmd "ProofGeneral.inform_file_retracted \"%s\";")
+ proof-shell-inform-file-processed-cmd "ProofGeneral.inform_file_processed \"%e\";"
+ proof-shell-inform-file-retracted-cmd "ProofGeneral.inform_file_retracted \"%e\";")
(add-hook 'proof-activate-scripting-hook 'isar-activate-scripting))