diff options
| -rw-r--r-- | doc/PG-adapting.texi | 37 | ||||
| -rw-r--r-- | generic/proof-config.el | 52 | ||||
| -rw-r--r-- | generic/proof-script.el | 16 | ||||
| -rw-r--r-- | generic/proof-shell.el | 3 |
4 files changed, 1 insertions, 107 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 6f9c8142..025b4b07 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -1814,43 +1814,6 @@ on @samp{@code{proof-shell-eager-annotation-start}} and Set to nil to disable. @end defvar -@c TEXI DOCSTRING MAGIC: proof-shell-set-elisp-variable-regexp -@defvar proof-shell-set-elisp-variable-regexp -Matches output telling Proof General to set some variable.@* -This allows the proof assistant to configure Proof General directly -and dynamically. (It's also a fantastic backdoor security risk). - -More precisely, this should match a string which is bounded by -matches on @samp{@code{proof-shell-eager-annotation-start}} and -@samp{@code{proof-shell-eager-annotation-end}}. - -If the regexp matches output from the proof assistant, there should be -two match strings: (@code{match-string} 1) should be the name of the elisp -variable to be set, and (@code{match-string} 2) should be the value of the -variable (which will be evaluated as a Lisp expression). - -A good markup for the second string is to delimit with #'s, since -these are not valid syntax for elisp evaluation. - -Elisp errors will be trapped when evaluating; set -@samp{@code{proof-general-debug}} to be informed when this happens. - -Example uses are to adjust PG's internal copies of proof assistant's -settings, or to make automatic dynamic syntax adjustments in Emacs to -match changes in theory, etc. - -If you pick a dummy variable name (e.g. @samp{proof-dummy-setting}) you -can just evaluation arbitrary elisp expressions for their side -effects, to adjust menu entries, or even launch auxiliary programs. -But use with care -- there is no protection against catastrophic elisp! - -This setting could also be used to move some configuration settings -from PG to the prover, but this is not really supported (most settings -must be made before this mechanism will work). In future, the PG -standard protocol, @var{pgip}, will use this mechanism for making all -settings. -@end defvar - @c TEXI DOCSTRING MAGIC: proof-shell-theorem-dependency-list-regexp @defvar proof-shell-theorem-dependency-list-regexp Matches output telling Proof General about dependencies.@* diff --git a/generic/proof-config.el b/generic/proof-config.el index 8d5f9762..9632a268 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -696,20 +696,6 @@ needed for Coq." :type 'boolean :group 'proof-script) -(defcustom proof-script-evaluate-elisp-comment-regexp "ELISP: -- \\(.*\\) --" - "Matches text within a comment telling Proof General to evaluate some code. -This allows Emacs Lisp to be executed during scripting. -\(It's also a fantastic backdoor security risk). - -If the regexp matches text inside a comment, there should be -one subexpression match string, which will contain elisp code -to be evaluated. - -Elisp errors will be trapped when evaluating; set -`proof-general-debug' to be informed when this happens." - :type 'regexp - :group 'proof-script) - ;; ;; Proof script indentation ;; @@ -1345,44 +1331,6 @@ match data triggered by `proof-shell-retract-files-regexp'." :type 'string :group 'proof-shell) -(defcustom proof-shell-set-elisp-variable-regexp nil - "Matches output telling Proof General to set some variable. -This allows the proof assistant to configure Proof General directly -and dynamically. (It's also a fantastic backdoor security risk). - -More precisely, this should match a string which is bounded by -matches on `proof-shell-eager-annotation-start' and -`proof-shell-eager-annotation-end'. - -If the regexp matches output from the proof assistant, there should be -two match strings: (match-string 1) should be the name of the elisp -variable to be set, and (match-string 2) should be the value of the -variable (which will be evaluated as a Lisp expression). - -A good markup for the second string is to delimit with #'s, since -these are not valid syntax for elisp evaluation. - -Elisp errors will be trapped when evaluating; set -`proof-general-debug' to be informed when this happens. - -Example uses are to adjust PG's internal copies of proof assistant's -settings, or to make automatic dynamic syntax adjustments in Emacs to -match changes in theory, etc. - -If you pick a dummy variable name (e.g. `proof-dummy-setting') you -can just evaluation arbitrary elisp expressions for their side -effects, to adjust menu entries, or even launch auxiliary programs. -But use with care -- there is no protection against catastrophic elisp! - -This setting could also be used to move some configuration settings -from PG to the prover, but this is not really supported (most settings -must be made before this mechanism will work). In future, the PG -standard protocol, PGIP, will use this mechanism for making all -settings." - :type '(choice (const nil) regexp) - :group 'proof-shell) - - (defcustom proof-shell-match-pgip-cmd nil "Regexp used to match PGIP command from proof assistant. diff --git a/generic/proof-script.el b/generic/proof-script.el index a5109be7..87a9975b 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1459,21 +1459,7 @@ Argument SPAN has just been processed." (span-set-property span 'id (intern id)) (span-set-property span 'idiom 'comment) (let ((proof-shell-last-output "")) ; comments not sent, no last output - (pg-set-span-helphighlights bodyspan)) - - ;; possibly evaluate some arbitrary Elisp. SECURITY RISK! - (save-match-data - (setq str (buffer-substring-no-properties (span-start span) - (span-end span))) - (if (proof-string-match-safe proof-script-evaluate-elisp-comment-regexp str) - (condition-case nil - (eval (car (read-from-string (match-string-no-properties 1 str))) - t) - (t (proof-debug - (concat - "lisp error when obeying proof-shell-evaluate-elisp-comment-regexp: \n" - (prin1-to-string (match-string-no-properties 1)) - "\n")))))))) + (pg-set-span-helphighlights bodyspan)))) (defun proof-done-advancing-save (span) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index af9b50e0..e39837c0 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1258,9 +1258,6 @@ ends with text matching `proof-shell-eager-annotation-end'." ((proof-looking-at-safe proof-shell-clear-goals-regexp) (proof-clean-buffer proof-goals-buffer)) - ((proof-looking-at-safe proof-shell-set-elisp-variable-regexp) - (proof-shell-process-urgent-message-elisp)) - ((proof-looking-at-safe proof-shell-match-pgip-cmd) (pg-pgip-process-packet ;; NB: xml-parse-region ignores junk before XML |