proof-try-command is deprecated

4 files changed, 71 insertions, 67 deletions

diff --git a/CHANGES b/CHANGES
index b3ae194b..a3772345 100644
--- a/CHANGES
+++ b/CHANGES
@@ -24,6 +24,10 @@ Generic Changes
 * Menus and keybindings have been reorganized.  
   Now keybindings invoke the same functions as the toolbar.
 
+* Command C-c C-t (proof-try-command) removed in favour of C-c C-v
+  (proof-execute-minibuffer-cmd), which now possibly uses the
+  filter proof-state-preserving-p to check that a command is safe.
+
 * Terminal string now automatically added to command for C-c C-v 
 
 * Cleaned up example files so all demonstrate same theorem "conj_comms".
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 2b005810..d140173f 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1128,8 +1128,6 @@ from a proof script.  Here are the keybindings and functions.
 @code{proof-help}
 @item C-c C-c
 @code{proof-interrupt-process}
-@item C-c t
-@code{proof-try-command}
 @item C-c C-v
 @code{proof-execute-minibuffer-cmd}
 @item C-c C-f
@@ -1167,21 +1165,6 @@ Issues a command based on @var{arg} to the assistant, using @code{proof-find-the
 The user is prompted for an argument.
 @end deffn
 
-
-@c TEXI DOCSTRING MAGIC: proof-try-command
-@deffn Command proof-try-command &optional unclosed-comment-fun
-Process the command at point, but don't add it to the locked region. 
-
-Supplied to let the user to test the types and values of
-expressions. Checks via the function @code{proof-state-preserving-p} that the
-command won't change the proof state, but this isn't guaranteed to be
-foolproof and may cause Proof General to lose sync with the prover.
-
-Default action if inside a comment is just to go until the start of
-the comment. If you want something different, put it inside
-@var{unclosed-comment-fun}.
-@end deffn
-
 @c TEXI DOCSTRING MAGIC: proof-execute-minibuffer-cmd
 @deffn Command proof-execute-minibuffer-cmd 
 Prompt for a command in the minibuffer and send it to proof assistant.@*
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 6b370382..64eae290 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -715,7 +715,9 @@ This is used to handle nested goals allowed by some provers."
   :group 'proof-script)
 
 (defcustom proof-state-preserving-p nil
-  "A predicate, non-nil if its argument (a command) preserves the proof state."
+  "A predicate, non-nil if its argument (a command) preserves the proof state.
+If set, used by proof-execute-minibuffer-cmd to filter out scripting
+commands which should be entered directly into the script itself."
   :type 'function
   :group 'proof-script)
 
diff --git a/generic/proof-script.el b/generic/proof-script.el
index cfdb6e66..7afaf7c4 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1168,51 +1168,6 @@ command."
 	   (setq span (span-at (point) 'type))))
     (proof-retract-target span delete-region)))
 
-;;         proof-try-command                                        ;;
-;;         this isn't really in the spirit of script management,    ;;
-;;         but sometimes the user wants to just try an expression   ;;
-;;         without having to undo it in order to try something      ;;
-;;         different. Of course you can easily lose sync by doing   ;;
-;;         something here which changes the proof state             ;;
-
-(defun proof-done-trying (span)
-  "Callback for proof-try-command."
-  (delete-span span)
-  (proof-detach-queue))
-			
-(defun proof-try-command (&optional unclosed-comment-fun) 
-  "Process the command at point, but don't add it to the locked region. 
-
-Supplied to let the user to test the types and values of
-expressions. Checks via the function proof-state-preserving-p that the
-command won't change the proof state, but this isn't guaranteed to be
-foolproof and may cause Proof General to lose sync with the prover.
-
-Default action if inside a comment is just to go until the start of
-the comment. If you want something different, put it inside
-UNCLOSED-COMMENT-FUN."
-  (interactive)
-  (proof-shell-ready-prover)
-  (proof-activate-scripting)
-  (let ((pt (point)) semis test)
-    (save-excursion
-      (if (proof-only-whitespace-to-locked-region-p)
-	  (progn (goto-char pt)
-		 (error "I don't know what I should be doing in this buffer!")))
-      (setq semis (proof-segment-up-to (point))))
-    (if (and unclosed-comment-fun (eq 'unclosed-comment (car semis)))
-	(funcall unclosed-comment-fun)
-      (if (eq 'unclosed-comment (car semis)) (setq semis (cdr semis)))
-      (if (null semis) 
-	  (error "I don't know what I should be doing in this buffer!"))
-      (setq test (car semis))
-      (if (not (funcall proof-state-preserving-p (nth 1 test)))
-	  (error "Command is not state preserving, I won't try it."))
-      (goto-char (nth 2 test))
-      (let ((vanillas (proof-semis-to-vanillas (list test)
-					       'proof-done-trying)))
-	(proof-start-queue (proof-unprocessed-begin) (point) vanillas)))))
-
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -1382,8 +1337,10 @@ Only for use by consenting adults."
   "Prompt for a command in the minibuffer and send it to proof assistant.
 The command isn't added to the locked region.
 
-Warning! No checking whatsoever is done on the command, so this is
-even more dangerous than proof-try-command."
+If proof-state-preserving-p is configured, it is used as a check
+that the command will be safe to execute, in other words, that
+it won't ruin synchronization.  If applied to the command it 
+returns false, then an error message is given."
   (interactive)
   (let (cmd)
     ;; FIXME note: removed ready-prover call since it's done by
@@ -1391,13 +1348,16 @@ even more dangerous than proof-try-command."
     ;; (proof-shell-ready-prover)
     ;; was (proof-check-process-available 'relaxed) 
     (setq cmd (read-string "Command: " nil 'proof-minibuffer-history))
+    (if (and
+	 proof-state-preserving-p
+	 (not (funcall proof-state-preserving-p cmd)))
+	  (error "Command is not state preserving, I won't execute it!"))
     (proof-shell-invisible-command 
      (if proof-terminal-string
 	 (concat cmd proof-terminal-string)
        cmd))))
 
 
-
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -1800,7 +1760,6 @@ Otherwise just do proof-restart-buffers to delete some spans from memory."
 ;;;; (define-key map [(control c) (control n)] 'proof-assert-next-command-interactive)
 ;; FIXME : This ought to be set to 'proof-assert-until point
 (define-key map [(control c) (return)]	  'proof-assert-next-command-interactive)
-(define-key map [(control c) (control t)] 'proof-try-command)
 ;; FIXME: The following two functions should be unified.
 (define-key map [(control c) ?u]	  'proof-retract-until-point-interactive)
 ;;;; (define-key map [(control c) (control u)] 'proof-undo-last-successful-command-interactive)
@@ -1981,6 +1940,62 @@ finish setup which depends on specific proof assistant configuration."
       (setq buffer-offer-save t)))
 
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; FIXME FIXME FIXME da:
+;;
+;; want to remove this function
+;; but at the moment it's used by
+;; plastic instantiation.  Try
+;; to persuade P.C. that we can
+;; live without it?
+
+
+;;         proof-try-command                                        ;;
+;;         this isn't really in the spirit of script management,    ;;
+;;         but sometimes the user wants to just try an expression   ;;
+;;         without having to undo it in order to try something      ;;
+;;         different. Of course you can easily lose sync by doing   ;;
+;;         something here which changes the proof state             ;;
+
+(defun proof-done-trying (span)
+  "Callback for proof-try-command."
+  (delete-span span)
+  (proof-detach-queue))
+			
+(defun proof-try-command (&optional unclosed-comment-fun) 
+  "Process the command at point, but don't add it to the locked region. 
+
+Supplied to let the user to test the types and values of
+expressions. Checks via the function proof-state-preserving-p that the
+command won't change the proof state, but this isn't guaranteed to be
+foolproof and may cause Proof General to lose sync with the prover.
+
+Default action if inside a comment is just to go until the start of
+the comment. If you want something different, put it inside
+UNCLOSED-COMMENT-FUN."
+  (interactive)
+  (proof-shell-ready-prover)
+  (proof-activate-scripting)
+  (let ((pt (point)) semis test)
+    (save-excursion
+      (if (proof-only-whitespace-to-locked-region-p)
+	  (progn (goto-char pt)
+		 (error "I don't know what I should be doing in this buffer!")))
+      (setq semis (proof-segment-up-to (point))))
+    (if (and unclosed-comment-fun (eq 'unclosed-comment (car semis)))
+	(funcall unclosed-comment-fun)
+      (if (eq 'unclosed-comment (car semis)) (setq semis (cdr semis)))
+      (if (null semis) 
+	  (error "I don't know what I should be doing in this buffer!"))
+      (setq test (car semis))
+      (goto-char (nth 2 test))
+      (let ((vanillas (proof-semis-to-vanillas (list test)
+					       'proof-done-trying)))
+	(proof-start-queue (proof-unprocessed-begin) (point) vanillas)))))
+
+
+
 (provide 'proof-script)
 ;; proof-script.el ends here.