diff options
| -rw-r--r-- | generic/proof-config.el | 15 | ||||
| -rw-r--r-- | generic/proof-script.el | 18 |
2 files changed, 31 insertions, 2 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 2bd15a77..7db11cba 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -725,6 +725,20 @@ assistant, for example, to compile a completed file." :type '(repeat function) :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 ;; @@ -1395,6 +1409,7 @@ settings." :type '(choice nil regexp) :group 'proof-shell) + (defcustom proof-shell-match-pgip-cmd nil "Regexp used to match PGIP command from proof assistant. The matching string will be parsed as XML and then processed by diff --git a/generic/proof-script.el b/generic/proof-script.el index 47ddd9bb..5eaa6c2a 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1348,13 +1348,27 @@ Argument SPAN has just been processed." (+ (length comment-start) (span-start span)) (- (span-end span) (max 1 (length comment-end))))) - (id (proof-next-element-id 'comment))) + (id (proof-next-element-id 'comment)) + str) (pg-add-element "comment" id bodyspan) (span-set-property span 'id (intern id)) - (span-set-property span 'idiom 'comment))) + (span-set-property span 'idiom 'comment) ;; this tries to extract last output, which is wrong for comments. ;; (pg-set-span-helphighlights span) + ;; 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 (proof-debug + (concat + "lisp error when obeying proof-shell-evaluate-elisp-comment-regexp: \n" + (print1-to-string (match-string-no-properties 1)) + "\n")))))))) + (defun proof-done-advancing-save (span) "A subroutine of `proof-done-advancing'. Add info for save span SPAN." |