Added proof-execute-minibuffer-cmd and scripting minor mode.

4 files changed, 173 insertions, 26 deletions

diff --git a/coq.el b/coq.el
index 0ff894fb..ec27e86c 100644
--- a/coq.el
+++ b/coq.el
@@ -3,6 +3,9 @@
 ;; Author: Healfdene Goguen and Thomas Kleymann
 
 ;; $Log$
+;; Revision 1.12  1997/11/24 19:15:08  djs
+;; Added proof-execute-minibuffer-cmd and scripting minor mode.
+;;
 ;; Revision 1.11  1997/11/20 13:03:08  hhg
 ;; Added coq-global-p for global declarations and definitions.  These now
 ;; get lifted in the same way as lemmas.
@@ -392,7 +395,124 @@ Require Emacs."
   (insert "Apply "))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;   Lego shell startup and exit hooks                              ;;
+;;   Indentation                                                    ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; This is quite different from sml-mode, but borrows some bits of
+;; code.  It's quite a lot less general, but works with nested
+;; comments.
+
+;; parse-to-point:
+;; If from is nil, parsing starts from locked-end. Otherwise state
+;; must contain a valid triple.
+
+(defun coq-parse-to-point (&optional from state)
+  (let ((comment-level 0) (stack (list (list nil 0)))
+	(end (point)) instring c)
+    (save-excursion
+      (if (null from)
+	  (proof-goto-end-of-locked)
+	(goto-char from)
+	(setq instring (car state)
+	      comment-level (nth 1 state)
+	      stack (nth 2 state)))
+      (while (< (point) end)
+	(setq c (char-after (point)))
+	(cond 
+	 (instring 
+	  (if (eq c ?\") (setq instring nil)))
+	 (t (cond
+	     ((eq c ?\()
+	      (if (looking-at "(\\*") (progn 
+					(incf comment-level)
+					(forward-char))
+		(if (>= 0 comment-level) 
+		    (setq stack (cons (list c (point)) stack)))))
+	     ((and (eq c ?\*) (looking-at "\\*)"))
+	      (decf comment-level)
+	      (forward-char))
+	     ((> comment-level 0))
+
+	     ((and (eq c ?c) (looking-at "case"))
+	      (setq stack (cons (list c (point)) stack)))
+	     ((and (eq c ?e) (looking-at "end") (eq (car (car stack)) ?c))
+	      (setq stack (cdr stack)))
+
+	     ((eq c ?I) (looking-at "Inductive")
+	      (setq stack (cons (list c (point)) stack)))
+	     ((and (eq c ?.)  (eq (car (car stack)) ?I))
+	      (setq stack (cdr stack)))	     
+	     ((eq c ?\") (setq instring t))
+	     ((or (eq c ?\{) (eq c ?\[))
+	      (setq stack (cons (list c (point)) stack)))
+	     ((or (eq c ?\)) (eq c ?\}) (eq c ?\]))
+	      (setq stack (cdr stack))))))
+	(forward-char))
+    (list instring comment-level stack))))
+      
+(defun coq-stack-to-indent (stack)
+  (cond
+   ((null stack) 0)
+   ((null (car (car stack)))
+    (nth 1 (car stack)))
+   (t (let ((col (save-excursion
+		   (goto-char (nth 1 (car stack)))
+		   (current-column))))
+	(cond
+	 ((eq (car (car stack)) ?c)
+	  (save-excursion (move-to-column (current-indentation))
+			  (cond 
+			   ((eq (char-after (point)) ?|) (+ col 3))
+			   ((looking-at "end") col)
+			   (t (+ col 5)))))	  
+	 ((eq (car (car stack)) ?I)
+	  (+ col (if (eq ?| (save-excursion 
+			      (move-to-column (current-indentation))
+			      (char-after (point)))) 8 10)))
+	 (t (1+ col)))))))
+
+
+(defun coq-indent-line ()
+  (interactive)
+  (save-excursion
+    (beginning-of-line)
+    (if (< (point) (proof-locked-end))
+	(error "can't indent locked region!"))
+    (let* ((state (coq-parse-to-point))
+	   (beg (point))
+	   (indent (cond ((car state) 1)
+			 ((> (nth 1 state) 0) 1)
+			 (t (coq-stack-to-indent (nth 2 state))))))
+      (skip-chars-forward "\t ")
+      (delete-region beg (point))
+      (indent-to indent)))
+  (if (< (current-column) (current-indentation))
+      (skip-chars-forward "\t ")))
+
+(defun coq-indent-region (start end)
+  (interactive "r")
+  (save-excursion
+    (goto-char start)
+    (beginning-of-line)
+    (if (< (point) (proof-locked-end))
+	(error "can't indent locked region!"))
+    (let* ((beg (point))
+	   (state (coq-parse-to-point))
+	   indent)
+      (while (<= (point) end)
+	(setq indent (cond ((car state) 1)
+			   ((> (nth 1 state) 0) 1)
+			   (t (coq-stack-to-indent (nth 2 state)))))	
+	(skip-chars-forward "\t ")
+	(delete-region beg (point))
+	(indent-to indent)
+	(end-of-line)
+	(if (< (point) (point-max)) (forward-char))
+	(setq state (coq-parse-to-point beg state)
+	      beg (point))))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;   Coq shell startup and exit hooks                               ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (defvar coq-shell-current-line-width nil
@@ -469,17 +589,16 @@ Require Emacs."
 
   (proof-config-done)
 
-  (define-key (current-local-map) [(meta tab)]
-    (if (fboundp 'complete-tag)
-	'complete-tag		; Emacs 19.31 (superior etags)
-      'tag-complete-symbol))	;XEmacs 19.13 (inferior etags)
+;  (define-key (current-local-map) [(meta tab)]
+;    (if (fboundp 'complete-tag)
+;	'complete-tag		; Emacs 19.31 (superior etags)
+;      'tag-complete-symbol))	;XEmacs 19.13 (inferior etags)
   (define-key (current-local-map) [(control c) (control p)] 'coq-prf)
   (define-key (current-local-map) [(control c) c] 'coq-ctxt)
   (define-key (current-local-map) [(control c) h] 'coq-help)
   (define-key (current-local-map) [(control c) I] 'coq-Intros)
-  (define-key (current-local-map) "\C-ca"    'coq-Apply)
-
-;;  (define-key (current-local-map) [tab]      'lego-indent-line)
+  (define-key (current-local-map) [(control c) a] 'coq-Apply)
+  (define-key (current-local-map) [tab]      'coq-indent-line)
 
 ;; outline
   
diff --git a/lego.el b/lego.el
index 1458506e..7e4bc6ab 100644
--- a/lego.el
+++ b/lego.el
@@ -5,6 +5,9 @@
 
 
 ;; $Log$
+;; Revision 1.31  1997/11/24 19:15:11  djs
+;; Added proof-execute-minibuffer-cmd and scripting minor mode.
+;;
 ;; Revision 1.30  1997/11/20 13:04:59  hhg
 ;; Added lego-global-p as always false, but for consistency with Coq mode.
 ;; Changed [meta (control i)] to [meta tab] in key definition.
@@ -415,7 +418,7 @@
 ;; code.  It's quite a lot less general, but works with nested
 ;; comments.
 
-;; proof-parse-to-point:
+;; parse-to-point:
 ;; If from is nil, parsing starts from locked-end. Otherwise state
 ;; must contain a valid triple.
 
@@ -565,7 +568,6 @@
 
   (proof-config-done)
 
-  ; (meta (control i)) causes emacs to fail, maybe it raises an exception
   (define-key (current-local-map) [(meta tab)]
     (if (fboundp 'complete-tag)
 	'complete-tag		; Emacs 19.31 (superior etags)
diff --git a/proof-dependencies.el b/proof-dependencies.el
index d3dcddb3..39188802 100644
--- a/proof-dependencies.el
+++ b/proof-dependencies.el
@@ -89,7 +89,8 @@
   (set-extent-property proof-locked-ext 'read-only nil))
 
 (defsubst proof-detach-queue ()
-  (detach-extent proof-queue-ext))
+  (if proof-queue-ext
+      (detach-extent proof-queue-ext)))
 
 (defsubst proof-set-queue-endpoints (start end)
   (set-extent-endpoints proof-queue-ext start end))
@@ -103,8 +104,10 @@
 			end)) 
 
 (defsubst proof-detach-segments ()
-  (detach-extent proof-queue-ext)
-  (detach-extent proof-locked-ext))
+  (if proof-queue-ext
+      (detach-extent proof-queue-ext))
+  (if proof-locked-ext
+      (detach-extent proof-locked-ext)))
 
 (defsubst proof-set-locked-end (end)
   (set-extent-endpoints proof-locked-ext (point-min) end))
diff --git a/proof.el b/proof.el
index 965df9fd..89ec0aa9 100644
--- a/proof.el
+++ b/proof.el
@@ -9,6 +9,9 @@
 
 
 ;; $Log$
+;; Revision 1.27  1997/11/24 19:15:16  djs
+;; Added proof-execute-minibuffer-cmd and scripting minor mode.
+;;
 ;; Revision 1.26  1997/11/20 16:47:48  hhg
 ;; Added proof-global-p to test whether a 'vanilla should be lifted above
 ;; active lemmas.
@@ -263,6 +266,8 @@
 (defvar proof-included-files-list nil 
   "Files currently included in proof process")
 
+(deflocal proof-active-buffer-fake-minor-mode nil
+  "An indication in the modeline that this is the *active* buffer")
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;               Bridging the emacs19/xemacs gulf                   ;;
@@ -355,6 +360,17 @@
 	(set-buffer proof-pbp-buffer)
 	(funcall proof-mode-for-pbp))
 
+      (setq proof-script-buffer (current-buffer))
+      (proof-init-segmentation)
+      (setq proof-active-buffer-fake-minor-mode t)
+      (redraw-modeline)
+
+      (or (assq 'proof-active-buffer-fake-minor-mode minor-mode-alist)
+	  (setq minor-mode-alist
+		(append minor-mode-alist
+			(list '(proof-active-buffer-fake-minor-mode 
+				" Scripting")))))
+
       (message 
        (format "Starting %s process... done." proc)))))
   
@@ -652,9 +668,10 @@
 
 (defun proof-check-process-available ()
   (if (proof-shell-live-buffer)
-      (if proof-shell-busy (error "Proof Process Busy!")))
-  (if (not (eq proof-script-buffer (current-buffer)))
-      (error "Don't own proof process"))
+      (cond
+       (proof-shell-busy (error "Proof Process Busy!"))
+       ((not (eq proof-script-buffer (current-buffer)))
+	(error "Don't own proof process"))))
   (if (not (eq proof-buffer-type 'script))
       (error "Must be running in a script buffer")))
 
@@ -806,10 +823,6 @@ at the end of locked region (after inserting a newline)."
   (cond
    ((eq proof-script-buffer (current-buffer))
     nil)
-   ((or (null proof-script-buffer) (not (buffer-live-p proof-script-buffer)))
-    (setq proof-script-buffer (current-buffer))
-    (proof-init-segmentation)
-    nil)
    (t 
     (let ((flist proof-included-files-list) 
 	  (file (expand-file-name (buffer-file-name))) ext cmd)
@@ -825,9 +838,12 @@ at the end of locked region (after inserting a newline)."
 	(setq cmd (if (and ext (not (eq (span-property ext 'type) 'goalsave)))
 		      proof-kill-goal-command ""))
 	(proof-detach-segments)
-	(delete-spans (point-min) (point-max) 'type))      
+	(delete-spans (point-min) (point-max) 'type)
+	(setq proof-active-buffer-fake-minor-mode nil))      
       (setq proof-script-buffer (current-buffer))
       (proof-detach-segments)
+      (proof-init-segmentation)
+      (setq proof-active-buffer-fake-minor-mode t)
 
       (cond 
        (flist
@@ -1151,18 +1167,24 @@ deletes the region corresponding to the proof sequence."
     (proof-set-locked-end (point))
     (delete-spans (proof-locked-end) (point-max) 'type)))
 
+(defvar proof-minibuffer-history nil
+  "The last command read from the minibuffer")
 
+(defun proof-execute-minibuffer-cmd ()
+  (interactive)
+  (let (cmd)
+    (proof-check-process-available)
+    (setq cmd (read-string "Command: " nil 'proof-minibuffer-history))
+;     proof-minibuffer-history (cons cmd proof-minibuffer-history))
+    (proof-invisible-command cmd)))
 	  
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;          Active terminator minor mode                            ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-(defvar proof-active-terminator-minor-mode nil 
+(deflocal proof-active-terminator-minor-mode nil 
 "active terminator minor mode flag")
 
-(make-variable-buffer-local 'proof-active-terminator-minor-mode)
-(put 'proof-active-terminator-minor-mode 'permanent-local t)
-
 (defun proof-active-terminator-minor-mode (&optional arg)
   "Toggle PROOF's Active Terminator minor mode.
 With arg, turn on the Active Terminator minor mode if and only if arg
@@ -1254,7 +1276,8 @@ current command."
   (define-key proof-mode-map [(control c) (control t)] 'proof-try-command)
   (define-key proof-mode-map [(control c) u] 'proof-retract-until-point)
   (define-key proof-mode-map [(control c) (control u)] 'proof-undo-last-successful-command)
-  (define-key proof-mode-map [(control c) ?'] 'proof-goto-end-of-locked)
+  (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)
 
   ;; For fontlock
   (remove-hook 'font-lock-after-fontify-buffer-hook 'proof-zap-commas-buffer t)