diff options
| -rw-r--r-- | coq/coq.el | 62 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 33 | ||||
| -rw-r--r-- | generic/proof-config.el | 33 | ||||
| -rw-r--r-- | generic/proof-syntax.el | 3 | ||||
| -rw-r--r-- | isa/isa.el | 14 | ||||
| -rw-r--r-- | isar/isar.el | 10 |
6 files changed, 82 insertions, 73 deletions
@@ -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)) @@ -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)) |