From f4781c9dcabf44a31d8dd65d00e3a46d38867e68 Mon Sep 17 00:00:00 2001
From: Healfdene Goguen <da+pg-hhg@inf.ed.ac.uk>
Date: Thu, 15 Jan 1998 12:23:59 +0000
Subject: Updated method of defining proof-shell-cd to be consistent with other
 proof-assistant-dependent variables. Added ctrl-button1 to copy selected
 region to end of locked region

---
 lego.el  | 11 ++++++++++-
 proof.el | 22 ++++++++++++++++++----
 2 files changed, 28 insertions(+), 5 deletions(-)

diff --git a/lego.el b/lego.el
index 2de2ca5a..3ddfbe1c 100644
--- a/lego.el
+++ b/lego.el
@@ -5,6 +5,11 @@
 
 
 ;; $Log$
+;; Revision 1.34  1998/01/15 12:23:59  hhg
+;; Updated method of defining proof-shell-cd to be consistent with other
+;; proof-assistant-dependent variables.
+;; Added ctrl-button1 to copy selected region to end of locked region
+;;
 ;; Revision 1.33  1998/01/05 14:59:03  tms
 ;; fixed a bug in the indenting functions
 ;;
@@ -145,7 +150,7 @@
 
 ;; ----- lego-shell configuration options
 
-(defvar lego-prog-name "/home/tms/src/lego/bin/lego"
+(defvar lego-prog-name "/home/ctm/lego/bin/legoML"
   "*Name of program to run as lego.")
 
 (defvar lego-shell-working-dir ""
@@ -154,6 +159,9 @@
 (defvar lego-shell-prompt-pattern "^\\(Lego>[ \201]*\\)+"
   "*The prompt pattern for the inferior shell running lego.")
 
+(defvar lego-shell-cd "Cd \"%s\";"
+  "*Command of the inferior process to change the directory.") 
+
 (defvar lego-shell-abort-goal-regexp "KillRef: ok, not in proof state"
   "*Regular expression indicating that the proof of the current goal
   has been abandoned.")
@@ -635,6 +643,7 @@
 
 (defun lego-shell-mode-config ()
   (setq proof-shell-prompt-pattern lego-shell-prompt-pattern
+        proof-shell-cd lego-shell-cd
         proof-shell-abort-goal-regexp lego-shell-abort-goal-regexp
         proof-shell-proof-completed-regexp lego-shell-proof-completed-regexp
         proof-shell-error-regexp lego-error-regexp
diff --git a/proof.el b/proof.el
index d6391574..812a90a1 100644
--- a/proof.el
+++ b/proof.el
@@ -9,6 +9,11 @@
 
 
 ;; $Log$
+;; Revision 1.32  1998/01/15 12:23:57  hhg
+;; Updated method of defining proof-shell-cd to be consistent with other
+;; proof-assistant-dependent variables.
+;; Added ctrl-button1 to copy selected region to end of locked region
+;;
 ;; Revision 1.31  1998/01/12 11:07:53  tms
 ;; o added support for remote proof processes
 ;; o bound C-c C-z to 'proof-frob-locked-end
@@ -157,7 +162,7 @@
 ;;               Configuration                                      ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-(defvar proof-shell-cd "Cd \"%s\";"
+(defvar proof-shell-cd nil
   "*Command of the inferior process to change the directory.") 
 
 (defvar proof-prog-name-ask-p nil
@@ -494,6 +499,15 @@
       (incf a))
     (apply 'concat (nreverse ls))))
 
+(defun proof-send-span (event)
+  (interactive "e")
+  (let* ((ext (span-at (mouse-set-point event) 'type))
+	 (str (span-property ext 'cmd)))
+    (cond ((and (eq proof-script-buffer (current-buffer)) (not (null ext)))
+	   (proof-goto-end-of-locked)
+	   (cond ((eq (span-property ext 'type) 'vanilla)
+		  (insert str)))))))
+
 (defun pbp-construct-command ()
   (let* ((ext (span-at (point) 'proof))
 	 (top-ext (span-at (point) 'proof-top-element))
@@ -889,8 +903,6 @@ at the end of locked region (after inserting a newline and indenting)."
       (setq ext (prev-span ext 'type)))
     ext)))
     
-
-
 (defun proof-steal-process ()
   (proof-start-shell)
   (if proof-shell-busy (error "Proof Process Busy!"))
@@ -1376,6 +1388,7 @@ current command."
   (define-key proof-mode-map [(control c) (control u)] 'proof-undo-last-successful-command)
   (define-key proof-mode-map [(control c) (control v)] 'proof-execute-minibuffer-cmd)
   (define-key proof-mode-map [(control c) ?\'] 'proof-goto-end-of-locked)
+  (define-key proof-mode-map [(control button1)] 'proof-send-span)
   (define-key proof-mode-map [(control c) (control b)] 'proof-process-buffer)
   (define-key proof-mode-map [(control c) (control z)] 'proof-frob-locked-end)
 
@@ -1406,7 +1419,8 @@ current command."
   ;; If the proof process in invoked on a different machine e.g.,
   ;; for proof-prog-name="rsh fastmachine proofprocess", one needs
   ;; to adjust the directory:
-  (proof-shell-insert (format proof-shell-cd default-directory))
+  (and proof-shell-cd
+       (proof-shell-insert (format proof-shell-cd default-directory)))
 
   (if proof-shell-init-cmd
        (proof-shell-insert proof-shell-init-cmd))
-- 
cgit v1.2.3