From fd186f51e733964a2c0f826e7cd2bba006ea4e69 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 25 Apr 2000 13:15:25 +0000
Subject: Revert to indended fix for isa-retract-thy-file.

---
 isa/isa.el | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/isa/isa.el b/isa/isa.el
index a476c5d1..a197bb73 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -175,8 +175,6 @@ and script mode."
      ;; Normal case: quotation for backslash, quote mark.
      '(("\\\\" . "\\\\") ("\""   . "\\\"")))
 
-
-   ;; FIXME: the next two are probably only good for NJ/SML
    proof-shell-interrupt-regexp         "Interrupt"
    proof-shell-error-regexp		"^\364\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception-\\( \\|$\\)"
    
@@ -407,7 +405,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 \"%r\";"
   "Sent to Isabelle to forget theory file and descendants.
 Resulting output from Isabelle will be parsed by Proof General."
   :type 'string
@@ -421,9 +419,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
-- 
cgit v1.2.3