Added proof-shell-set-elisp-variable-regexp

2 files changed, 71 insertions, 8 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index cd2b8f8a..4743eac6 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -620,6 +620,9 @@ Suggestion: this can be set a function called by `pre-shell-start-hook'."
   "Mode for proof script buffers.
 This is used by Proof General to find out which buffers 
 contain proof scripts.
+The regular name for this is <PA>-mode.  If you use any of the
+convenience macros Proof General provides for defining commands
+etc, then you should stick to this name.
 Suggestion: this can be set in the script mode configuration."
   :type 'function
   :group 'prover-config)
@@ -1650,12 +1653,48 @@ to do syntax highlighting with font-lock."
   :type 'boolean
   :group 'proof-shell)
 
+(defcustom proof-shell-set-elisp-variable-regexp nil
+  "Regexp matching output telling Proof General to set some variable.
+This allows the proof assistant to configure Proof General directly
+and dynamically.  
+
+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-show-debug-messages 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 nil regexp)
+  :group 'proof-shell)
+
 (defcustom proof-shell-theorem-dependency-list-regexp nil
   "Regexp matching output telling Proof General what the dependencies are.  
-This is so that the dependent theorems can be highlighted.  Set to nil to disable."
+This is so that the dependent theorems can be highlighted somehow.  
+Set to nil to disable.
+This is an experimental feature, currently work-in-progress."
   :type '(choice nil regexp)
   :group 'proof-shell)
 
+
 ;;
 ;; 5c. hooks and other miscellaneous customizations
 ;;
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index e85c4628..a63cd8c2 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1301,8 +1301,10 @@ Assume proof-script-buffer is active."
 
 (defun proof-shell-process-urgent-message (message)
   "Analyse urgent MESSAGE for various cases.
-Cases are: included file, retracted file, cleared response buffer, or
-if none of these apply, display it.
+Cases are: included file, retracted file, cleared response buffer, 
+variable setting or dependency list. 
+If none of these apply, display MESSAGE.
+
 MESSAGE should be a string annotated with 
 proof-shell-eager-annotation-start, proof-shell-eager-annotation-end."
     (cond
@@ -1336,7 +1338,7 @@ proof-shell-eager-annotation-start, proof-shell-eager-annotation-end."
       (if (and file (not (string= file "")))
 	  (proof-register-possibly-new-processed-file file))))
 
-   ;; Is the prover retracting across files?
+   ;; CASE retract: the prover is retracting across files
    ((and proof-shell-retract-files-regexp
 	 (string-match proof-shell-retract-files-regexp message))
     (let ((current-included proof-included-files-list))
@@ -1387,22 +1389,44 @@ proof-shell-eager-annotation-start, proof-shell-eager-annotation-end."
 	  )))
       ))
 
-   ;; Is the prover asking Proof General to clear the response buffer?
+   ;; CASE clear response: prover asks PG to clear response buffer
    ((and proof-shell-clear-response-regexp
 	 (string-match proof-shell-clear-response-regexp message)
 	 proof-response-buffer)
     ;; Erase response buffer and possibly its windows.
     (proof-shell-maybe-erase-response nil t t))
 
-   ;; Is the prover asking Proof General to clear the goals buffer?
+   ;; CASE clear goals: prover asks PG to clear goals buffer
    ((and proof-shell-clear-goals-regexp
 	 (string-match proof-shell-clear-goals-regexp message)
 	 proof-goals-buffer)
     ;; Erase goals buffer but and possibly its windows
     (proof-clean-buffer proof-goals-buffer))
    
-   ((if proof-shell-theorem-dependency-list-regexp 
-	(string-match proof-shell-theorem-dependency-list-regexp message))
+   ;; CASE variable setting: prover asks PG to set some variable 
+   ;; NB: no safety protection whatsoever here, we use blind faith
+   ;; that the prover will not send malicious elisp!!
+   ((and proof-shell-set-elisp-variable-regexp
+	 (string-match proof-shell-set-elisp-variable-regexp message))
+    (let 
+	((variable   (match-string 1 message))
+	 (expr	     (match-string 2 message)))
+      (condition-case err
+	  ;; Easiest way to do this seems to be to dump the lisp
+	  ;; string into another buffer -- no direct way to eval
+	  ;; from a string?
+	(with-temp-buffer
+	  (insert expr)
+	  (set (intern variable) (eval-last-sexp t)))
+	(t (proof-debug 
+	    (concat
+	     "lisp error when obeying proof-shell-set-elisp-variable: \n"
+	     "setting `" variable "'\n to: \n"
+	     expr "\n"))))))
+
+   ;; CASE theorem dependency: prover lists thms used in last proof
+   ((and proof-shell-theorem-dependency-list-regexp 
+	 (string-match proof-shell-theorem-dependency-list-regexp message))
       (setq proof-last-theorem-dependencies 
 	    (split-string (match-string 1 message))))