Remove evaluate-elisp-comment-regexp and set-elisp-variable-regexp

Closes GH-557.

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.@*

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.
 

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)

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