Altered proof-format-filename to add %e and %r specifiers.

1 files changed, 16 insertions, 4 deletions

diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index ae57888c..39a1d930 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -140,6 +140,8 @@ may assign this function to `after-change-function'."
 ;; Functions for doing something like "format" but with customizable
 ;; control characters.
 ;;
+;; Added for version 3.1 to help quote funny characters in filenames.
+;;
 
 (defun proof-format (alist string)
   "Format a string by matching regexps in ALIST against STRING"
@@ -155,13 +157,23 @@ may assign this function to `after-change-function'."
   string)
 
 (defun proof-format-filename (string filename)
-  "Format STRING by replacing %s or %e by expanded version of FILENAME.
-%e is special form meaning use proof-shell-string-escapes..
+  "Format STRING by replacing %e, %r by escaped version of FILENAME.
+
+%e uses the canonicalized expanded version of filename (including
+directory, using default-directory -- see `expand-file-name').
+
+%r uses the unadjusted (possibly relative) version of FILENAME.
+
+%s means the same as %e.
 
-We use expand-file-name to avoid problems with dumb
-proof assistants and ~"  
+Using %e can avoid problems with dumb proof assistants who don't
+understand ~, for example."  
   (proof-format 
    (list (cons "%s" (proof-format proof-shell-filename-escapes 
+				  (expand-file-name filename)))
+	 (cons "%e" (proof-format proof-shell-filename-escapes 
+				  (expand-file-name filename)))
+	 (cons "%r" (proof-format proof-shell-filename-escapes 
 				  (expand-file-name filename))))
    string))