Switch back to %s, rename proof-shell-string-escapes -> proof-shell-filename-escapes, and always apply for filename substn.

6 files changed, 82 insertions, 73 deletions

diff --git a/coq/coq.el b/coq/coq.el
index f649d858..014bd8ce 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -495,36 +495,38 @@
 
 
 (defun coq-shell-mode-config ()
-  (setq proof-shell-prompt-pattern coq-shell-prompt-pattern
-        proof-shell-cd-cmd coq-shell-cd
-        proof-shell-abort-goal-regexp coq-shell-abort-goal-regexp
-        proof-shell-proof-completed-regexp coq-shell-proof-completed-regexp
-        proof-shell-error-regexp coq-error-regexp
-	proof-shell-interrupt-regexp coq-interrupt-regexp
-        proof-shell-assumption-regexp coq-id
-        proof-shell-first-special-char ?\360
-        proof-shell-wakeup-char ?\371 ; done: prompt
-        ; The next three represent path annotation information
-	proof-shell-start-char ?\372 ; not done
-        proof-shell-end-char ?\373 ; not done
-        proof-shell-field-char ?\374 ; not done
-        proof-shell-goal-char ?\375 ; done
-	proof-shell-eager-annotation-start "\376" ; done
-	proof-shell-eager-annotation-start-length 1
-	proof-shell-eager-annotation-end "\377" ; done
-        proof-shell-annotated-prompt-regexp
-	(concat proof-shell-prompt-pattern
-		(char-to-string proof-shell-wakeup-char)) ; done
-        proof-shell-result-start "\372 Pbp result \373"
-        proof-shell-result-end "\372 End Pbp result \373"
-        proof-shell-start-goals-regexp "[0-9]+ subgoals?"
-        proof-shell-end-goals-regexp proof-shell-annotated-prompt-regexp
-        proof-shell-init-cmd coq-shell-init-cmd
-	proof-shell-restart-cmd coq-shell-restart-cmd
-	proof-analyse-using-stack t
-;;	proof-lift-global 'coq-lift-global
-	)
-
+  (setq 
+   proof-shell-prompt-pattern coq-shell-prompt-pattern
+   proof-shell-cd-cmd coq-shell-cd
+   proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\""   . "\\\""))
+   proof-shell-abort-goal-regexp coq-shell-abort-goal-regexp
+   proof-shell-proof-completed-regexp coq-shell-proof-completed-regexp
+   proof-shell-error-regexp coq-error-regexp
+   proof-shell-interrupt-regexp coq-interrupt-regexp
+   proof-shell-assumption-regexp coq-id
+   proof-shell-first-special-char ?\360
+   proof-shell-wakeup-char ?\371 ; done: prompt
+					; The next three represent path annotation information
+   proof-shell-start-char ?\372 ; not done
+   proof-shell-end-char ?\373 ; not done
+   proof-shell-field-char ?\374 ; not done
+   proof-shell-goal-char ?\375 ; done
+   proof-shell-eager-annotation-start "\376" ; done
+   proof-shell-eager-annotation-start-length 1
+   proof-shell-eager-annotation-end "\377" ; done
+   proof-shell-annotated-prompt-regexp
+   (concat proof-shell-prompt-pattern
+	   (char-to-string proof-shell-wakeup-char)) ; done
+   proof-shell-result-start "\372 Pbp result \373"
+   proof-shell-result-end "\372 End Pbp result \373"
+   proof-shell-start-goals-regexp "[0-9]+ subgoals?"
+   proof-shell-end-goals-regexp proof-shell-annotated-prompt-regexp
+   proof-shell-init-cmd coq-shell-init-cmd
+   proof-shell-restart-cmd coq-shell-restart-cmd
+   proof-analyse-using-stack t
+   ;;	proof-lift-global 'coq-lift-global
+   )
+  
   (coq-init-syntax-table)
   (setq font-lock-keywords coq-font-lock-keywords-1)
 
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index c9a1c271..b3c22fa6 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -3955,10 +3955,9 @@ need to bump up this value.
 @c TEXI DOCSTRING MAGIC: proof-shell-cd-cmd
 @defvar proof-shell-cd-cmd 
 Command to the proof assistant to change the working directory.@*
-The format character %s is replaced with the directory, and the
-@code{proof-terminal-char} is added on to the end.
-The format character %e is replaced by the directory, after applying
-escapes specified in @samp{@code{proof-shell-string-escapes}}, which see.
+The format character @samp{%s} is replaced with the directory, and the
+@code{proof-terminal-char} is added on to the end.  The escape sequences
+in @samp{@code{proof-shell-filename-escapes}} are applied to the filename.
 
 This setting is used to define the function @code{proof-cd} which 
 changes to the value of (@code{default-directory}) for script buffers.
@@ -3977,9 +3976,10 @@ for more details about the final two settings in this group,
 @c TEXI DOCSTRING MAGIC: proof-shell-inform-file-processed-cmd
 @defvar proof-shell-inform-file-processed-cmd 
 Command to the proof assistant to tell it that a file has been processed.@*
-The format character %s is replaced by a complete filename for a
+The format character @samp{%s} is replaced by a complete filename for a
 script file which has been fully processed interactively with
-Proof General.  
+Proof General.  The escape sequences in @samp{@code{proof-shell-filename-escapes}} 
+are applied to the filename.
 
 This is used to interface with the proof assistant's internal
 management of multiple files, so the proof assistant is kept aware of
@@ -3996,9 +3996,10 @@ See also: @code{proof-shell-inform-file-retracted-cmd},
 @c TEXI DOCSTRING MAGIC: proof-shell-inform-file-retracted-cmd
 @defvar proof-shell-inform-file-retracted-cmd 
 Command to the proof assistant to tell it that a file has been retracted.@*
-The format character %s is replaced by a complete filename for a
+The format character @samp{%s} is replaced by a complete filename for a
 script file which Proof General wants the prover to consider
-as not completely processed.
+as not completely processed. The escape sequences
+in @samp{@code{proof-shell-filename-escapes}} are applied to the filename.
 
 This is used to interface with the proof assistant's internal
 management of multiple files, so the proof assistant is kept aware of
@@ -4141,19 +4142,19 @@ used to help parse the goals buffer to annotate it for proof by pointing.
 @node Hooks and other settings
 @subsection Hooks and other settings
 
-@c TEXI DOCSTRING MAGIC: proof-shell-string-escapes
-@defvar proof-shell-string-escapes 
-A list of escapes that are applied for %e substitutions.@*
-This allows handling some special syntax for commands.
+@c TEXI DOCSTRING MAGIC: proof-shell-filename-escapes
+@defvar proof-shell-filename-escapes 
+A list of escapes that are applied to %s for filenames.@*
 A list of cons cells, car of which is string to be replaced
 by the cdr.
-For example, when directories are sent to Isabelle or HOL,
-they appear inside ML strings, so the backslash character must
+For example, when directories are sent to Isabelle, HOL, and Coq,
+they appear inside ML strings and the backslash character must
 be escaped.  The setting
 @lisp
-  '(("\\" . "@var{\\\\}"))
+  '(("\\" . "\\"))
 @end lisp
-achieves this.
+achieves this.  This does not apply to @var{lego}, which does not
+need  escapes.
 @end defvar
 
 @c TEXI DOCSTRING MAGIC: proof-shell-process-connection-type
diff --git a/generic/proof-config.el b/generic/proof-config.el
index ae4dfafd..191a5d13 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1144,9 +1144,8 @@ need to bump up this value."
 (defcustom proof-shell-cd-cmd nil
   "Command to the proof assistant to change the working directory.
 The format character `%s' is replaced with the directory, and the
-proof-terminal-char is added on to the end.
-The format character `%e' is replaced by the directory, after applying
-escapes specified in `proof-shell-string-escapes', which see.
+proof-terminal-char is added on to the end.  The escape sequences
+in `proof-shell-filename-escapes' are applied to the filename.
 
 This setting is used to define the function proof-cd which 
 changes to the value of (default-directory) for script buffers.
@@ -1163,9 +1162,8 @@ script every time scripting begins."
  "Command to the proof assistant to tell it that a file has been processed.
 The format character `%s' is replaced by a complete filename for a
 script file which has been fully processed interactively with
-Proof General.  
-(Use the format character `%e' instead to applying the escapes 
-specified in `proof-shell-string-escapes').
+Proof General.  The escape sequences in `proof-shell-filename-escapes' 
+are applied to the filename.
 
 This is used to interface with the proof assistant's internal
 management of multiple files, so the proof assistant is kept aware of
@@ -1185,9 +1183,8 @@ proof-shell-process-file, proof-shell-compute-new-files-list."
  "Command to the proof assistant to tell it that a file has been retracted.
 The format character `%s' is replaced by a complete filename for a
 script file which Proof General wants the prover to consider
-as not completely processed.
-(Use the format character `%e' instead to applying the escapes 
-specified in `proof-shell-string-escapes').
+as not completely processed. The escape sequences
+in `proof-shell-filename-escapes' are applied to the filename.
 
 This is used to interface with the proof assistant's internal
 management of multiple files, so the proof assistant is kept aware of
@@ -1463,16 +1460,18 @@ to do syntax highlighting with font-lock."
 ;; 5c. hooks and other miscellaneous customizations
 ;;
 
-(defcustom proof-shell-string-escapes '(("\\\\" . "\\\\"))
-  "A list of escapes that are applied for %e substitutions.
-This allows handling some special syntax for commands.
+(defcustom proof-shell-filename-escapes nil
+  "A list of escapes that are applied to %s for filenames.
 A list of cons cells, car of which is string to be replaced
 by the cdr.
-For example, when directories are sent to Isabelle or HOL,
-they appear inside ML strings, so the backslash character must
-be escaped.  The setting
-  '((\"\\\\\" . \"\\\\\\\\\"))
-achieves this."
+For example, when directories are sent to Isabelle, HOL, and Coq,
+they appear inside ML strings and the backslash character and
+quote characters must be escaped.  The setting
+  '((\"\\\\\\\\\" . \"\\\\\\\\\")
+    (\"\\\"\" . \"\\\\\\\"\"))
+achieves this.   This does not apply to LEGO, which does not
+need backslash escapes and does not allow filenames with
+quote characters."
   :type '(list (cons string string))
   :group 'proof-shell)
 
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index 69d08e7f..ae57888c 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -161,8 +161,7 @@ may assign this function to `after-change-function'."
 We use expand-file-name to avoid problems with dumb
 proof assistants and ~"  
   (proof-format 
-   (list (cons "%s" (expand-file-name filename))
-	 (cons "%e" (proof-format proof-shell-string-escapes 
+   (list (cons "%s" (proof-format proof-shell-filename-escapes 
 				  (expand-file-name filename))))
    string))
  
diff --git a/isa/isa.el b/isa/isa.el
index 1945f0d3..95479fd1 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 \"%e\";"
+   "ProofGeneral.inform_file_processed \"%s\";"
    proof-shell-inform-file-retracted-cmd 
-   "ProofGeneral.inform_file_retracted \"%e\";"))
+   "ProofGeneral.inform_file_retracted \"%s\";"))
 
 
 (defun isa-shell-mode-config-set-variables ()
@@ -142,7 +142,11 @@ and script mode."
    proof-shell-prompt-pattern		"^2?[ML-=#>]>? \372?"
 
    ;; for issuing command, not used to track cwd in any way.
-   proof-shell-cd-cmd			"Library.cd \"%e\""
+   proof-shell-cd-cmd			"Library.cd \"%s\""
+
+   ;; Escapes for filenames inside ML strings.
+   proof-shell-filename-escapes		
+   '(("\\\\" . "\\\\") ("\""   . "\\\""))
 
    ;; FIXME: the next two are probably only good for NJ/SML
    proof-shell-interrupt-regexp         "Interrupt"
@@ -251,7 +255,7 @@ and script mode."
   "Tell Isabelle to update current buffer's theory, and all ancestors."
   (proof-shell-invisible-command
    (proof-format-filename
-    (format "ProofGeneral.%supdate_thy_only \"%%e\";" (if try "try_" ""))
+    (format "ProofGeneral.%supdate_thy_only \"%%s\";" (if try "try_" ""))
     (file-name-sans-extension file))
    wait))
 
@@ -380,7 +384,7 @@ isa-proofscript-mode."
   (save-some-buffers)
   (isa-update-thy-only file nil nil))
 
-(defcustom isa-retract-thy-file-command "ThyInfo.remove_thy \"%e\";"
+(defcustom isa-retract-thy-file-command "ThyInfo.remove_thy \"%s\";"
   "Sent to Isabelle to forget theory file and descendants.
 Resulting output from Isabelle will be parsed by Proof General."
   :type 'string
diff --git a/isar/isar.el b/isar/isar.el
index f65b78cd..866bee75 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -242,7 +242,11 @@
    proof-shell-prompt-pattern		"^\\w*[>#] "
 
    ;; for issuing command, not used to track cwd in any way.
-   proof-shell-cd-cmd			"ML {* Library.cd \"%e\" *}"
+   proof-shell-cd-cmd			"ML {* Library.cd \"%s\" *}"
+
+   ;; Escapes for filenames inside ML strings.
+   proof-shell-filename-escapes		
+   '(("\\\\" . "\\\\") ("\""   . "\\\""))
 
    proof-shell-proof-completed-regexp   nil     ; n.a.
    proof-shell-interrupt-regexp         "\364\\*\\*\\* Interrupt\\|\360Interrupt"
@@ -299,8 +303,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 \"%e\";"
-   proof-shell-inform-file-retracted-cmd "ProofGeneral.inform_file_retracted \"%e\";")
+   proof-shell-inform-file-processed-cmd "ProofGeneral.inform_file_processed \"%s\";"
+   proof-shell-inform-file-retracted-cmd "ProofGeneral.inform_file_retracted \"%s\";")
   (add-hook 'proof-activate-scripting-hook 'isar-activate-scripting))