diff options
Diffstat (limited to 'generic/proof-config.el')
| -rw-r--r-- | generic/proof-config.el | 52 |
1 files changed, 0 insertions, 52 deletions
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. |