Emacs mode for lego

1 files changed, 490 insertions, 0 deletions

diff --git a/proof.el b/proof.el
new file mode 100644
index 00000000..e28bd595
--- /dev/null
+++ b/proof.el
@@ -0,0 +1,490 @@
+;; proof.el Major mode for proof assistants Copyright (C) 1994,
+;; 1995, 1996 LFCS Edinburgh. This version by Dilip Sequeira, by
+;; rearranging Thomas Schreiber's code.
+
+;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
+;; Time-stamp: <17 Oct 96 djs /home/lego/emacs/lego.el>
+;; Thanks to David Aspinall, Robert Boyer, Rod Burstall,
+;;           James McKinna, Mark Ruys, Martin Steffen, Perdita Stevens  
+
+
+(require 'compile)
+(require 'comint)
+(require 'etags)			
+
+(autoload 'w3-fetch "w3" nil t)
+(autoload 'easy-menu-define "easymenu")
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;               Configuration                                      ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defvar proof-shell-echo-input t
+  "If nil, input to the proof shell will not be echoed")
+
+(defvar proof-prog-name-ask-p nil
+  "*If t, you will be asked which program to run when the inferior
+ process starts up.")
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;  Variables used by proof mode, all auto-buffer-local             ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defmacro deflocal (var)
+ (list 'make-variable-buffer-local (list 'quote var))
+ (list 'defvar var 'nil))
+
+;; These have to be supplied to configure the mode properly
+
+(deflocal proof-terminal-char)
+
+(deflocal proof-shell-prog-name)
+(deflocal proof-shell-process-name)
+(deflocal proof-shell-prompt-pattern)
+(deflocal proof-shell-mode-is)
+
+(deflocal proof-comment-start)
+(deflocal proof-comment-end)
+
+;; Supply these if you want
+
+(make-local-hook 'proof-shell-pre-display-hook)
+(make-local-hook 'proof-shell-post-display-hook)
+(make-local-hook 'proof-shell-safe-send-hook)
+(make-local-hook 'proof-shell-exit-hook)
+
+;; These get computed in proof-mode-child-config-done
+
+(deflocal proof-terminal-string)
+(deflocal proof-shell-working-dir)
+(deflocal proof-re-end-of-cmd) 
+(deflocal proof-re-term-or-comment)
+(deflocal proof-shell-buffer-name)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;               Bridging the emacs19/xemacs gulf                   ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defvar running-xemacs  nil)
+(defvar running-emacs19 nil)
+
+(setq running-xemacs  (string-match "XEmacs\\|Lucid" emacs-version))
+(or running-xemacs
+    (setq running-emacs19 (string-match "^19\\." emacs-version)))
+
+;; courtesy of Mark Ruys 
+(defun emacs-version-at-least (major minor)
+  "Test if emacs version is at least major.minor"
+  (or (> emacs-major-version major)
+      (and (= emacs-major-version major) (>= emacs-minor-version minor)))
+)
+
+(defvar extended-shell-command-on-region
+  (emacs-version-at-least 19 29)
+  "Does `shell-command-on-region' optionally offer to output in an other buffer?")
+
+;; in case Emacs is not aware of read-shell-command-map
+(defvar read-shell-command-map
+  (let ((map (make-sparse-keymap)))
+    (if (not (fboundp 'set-keymap-parents))
+        (setq map (append minibuffer-local-map map))
+      (set-keymap-parents map minibuffer-local-map)
+      (set-keymap-name map 'read-shell-command-map))
+    (define-key map "\t" 'comint-dynamic-complete)
+    (define-key map "\M-\t" 'comint-dynamic-complete)
+    (define-key map "\M-?" 'comint-dynamic-list-completions)
+    map)
+  "Minibuffer keymap used by shell-command and related commands.")
+
+
+;; in case Emacs is not aware of the function read-shell-command
+(or (fboundp 'read-shell-command)
+    ;; from minibuf.el distributed with XEmacs 19.11
+    (defun read-shell-command (prompt &optional initial-input history)
+      "Just like read-string, but uses read-shell-command-map:
+\\{read-shell-command-map}"
+      (let ((minibuffer-completion-table nil))
+        (read-from-minibuffer prompt initial-input read-shell-command-map
+                              nil (or history
+                              'shell-command-history)))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;          A couple of small utilities                             ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defun string-to-list (s separator) 
+  "converts strings `s' separated by the character `separator' to a
+  list of words" 
+  (let ((end-of-word-occurence (string-match (concat separator "+") s)))
+    (if (not end-of-word-occurence)
+        (if (string= s "") 
+            nil
+          (list s))
+      (cons (substring s 0 end-of-word-occurence) 
+            (string-to-list 
+             (substring s
+                        (string-match (concat "[^" separator "]")
+                                      s end-of-word-occurence)) separator)))))
+
+
+(defun ids-to-regexp (l)
+  "transforms a non-empty list of identifiers `l' into a regular
+  expression matching any of its elements"
+  (let ((tail (cdr l))
+	(id (concat "\\<" (regexp-quote (car l)) "\\>")))
+    (if (atom tail) (regexp-quote id)
+      (concat id "\\|" (ids-to-regexp tail)))))
+
+(defun w3-remove-file-name (address)
+  "remove the file name in a World Wide Web address"
+  (string-match "://[^/]+/" address)
+  (concat (substring address 0 (match-end 0))
+          (file-name-directory (substring address (match-end 0)))))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;          A few random hacks                                      ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defun proof-skip-comments ()
+  (forward-comment (buffer-size))
+  (point))
+
+; Find the last real semicolon, or point-min, leaving the point after
+; the semi and any junk.  Returns nil if we seemto be inside a comment
+
+(defun proof-find-start-of-command ()
+   (if (re-search-backward proof-re-term-or-comment nil t)
+       (cond ((looking-at proof-terminal-string) 
+              (forward-char)
+	      (proof-skip-comments))
+	     ((looking-at   (substring proof-comment-start 0 1) nil))
+	     ((looking-at (substring proof-comment-end 0 1))
+	      (if (search-backward proof-comment-start nil t)
+		  (if (equal (point) (point-min)) 
+		      (proof-skip-comments))
+		    (backward-char)
+		    (proof-find-start-of-command))
+		(point)))
+     (goto-char (point-min))
+     (proof-skip-comments)))
+
+(defun proof-shell-buffer () (get-buffer proof-shell-buffer-name))
+
+(defun proof-display-buffer (buffer)
+  (let ((tmp-buffer (current-buffer)))
+    (display-buffer buffer)
+    (display-buffer tmp-buffer)))
+
+(defun proof-append-terminator (string)
+  (or (string-match proof-re-end-of-cmd string)
+      (setq string (concat string proof-terminal-string))))
+        
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;          Comint-style stuff: sending input to the process etc    ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defun proof-input-sender (proc string)
+  "Function to actually send to the PROOF process `proc' the `string'
+  submitted by the user. It then calls proof-shell-safe-send-hook if safe 
+  to do so."
+  (comint-simple-send proc string)
+  (and (string-match proof-re-end-of-cmd string)
+       (run-hooks 'proof-shell-safe-send-hook)))
+
+(defun proof-simple-send (string &optional silent)
+   "send `string' to the PROOF PROCESS.
+    If `silent' is enabled then `string' should not be echoed."
+  (or (get-process proof-shell-process-name) (proof-start-shell))
+  (let ((proof-buf (proof-shell-buffer)))
+    (if proof-buf
+	(save-excursion
+	  (progn
+	    (set-buffer proof-buf)
+	    (goto-char (point-max))
+	    (if (and proof-shell-echo-input (not silent))
+		(progn
+		  (princ string proof-buf)
+		  (comint-send-input))
+	      (proof-input-sender proof-shell-process-name string)
+	      )))
+      (message (format "No active %s process" proof-shell-process-name)))))
+
+(defun proof-simulate-send-region (point1 point2 &optional terminator)
+  "Send the area between point1 and point2 to the inferior shell running lego."
+  (let (str)
+    (setq str (buffer-substring point1 point2))
+    (and terminator (setq str (proof-append-terminator str)))
+    (proof-simple-send str)))
+
+;; proof-send-command tries to figure out where commands start and end
+;; without having to parse expressions. Actually needs re-writing.
+
+(defun proof-send-command ()
+  "Send current command to inferior shell."  
+
+  (interactive)
+  (let (start end)
+    (save-excursion
+      (setq start (proof-find-start-of-command))
+      (if start
+	  (setq end (search-forward proof-terminal-string nil t)))
+      (if (not end)
+	  (setq end (point-max))
+	(backward-char))
+      (run-hooks 'lego-shell-safe-send-hook)
+      (proof-simulate-send-region start end t))))
+
+(defun proof-send-line ()
+  "Send current line to inferior shell running proof"
+  (interactive)
+  (save-excursion
+    (let (start end)
+      (beginning-of-line 1)
+      (setq start (point))
+      (end-of-line 1)
+      (setq end (point))
+      (proof-simulate-send-region start end)))
+  (forward-line 1))
+  
+(defun proof-send-region ()
+  "Sends the current region to the inferior shell running proof and
+  appends a terminator if neccessary."
+  (interactive)
+  (let (start end)
+    (save-excursion
+      (setq end (point))
+      (exchange-point-and-mark)
+      (setq start (point)))
+    (proof-simulate-send-region start end t)))
+
+(defun proof-command (command)
+  (run-hooks 'lego-shell-safe-send-hook)
+  (let ((str (proof-append-terminator command)))
+       (insert str)
+  (proof-simple-send str)))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;  Starting, stopping, and interrupting the lego shell             ;;
+;;  There maybe more functionality here one day to support multiple ;;
+;;  subprocesses                                                    ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defun proof-start-shell ()
+  (let ((proof-buf (and proof-shell-process-name (proof-shell-buffer))))
+    (if (comint-check-proc proof-buf)
+        ()
+      (save-excursion
+        (and proof-prog-name-ask-p
+             (setq proof-shell-prog-name
+                   (read-shell-command "Run process: "
+                                       proof-shell-prog-name))))
+      (setq proof-shell-working-dir default-directory)
+      (or proof-shell-process-name
+          (setq proof-shell-process-name
+                (concat
+                 "Inferior "
+                 (substring proof-shell-prog-name
+                            (string-match "[^/]*$" proof-shell-prog-name)
+                            (string-match "$" proof-shell-prog-name)))))
+      (message (format "Starting %s process..." proof-shell-process-name))
+      
+      (proof-spawn-process proof-shell-prog-name 
+			 proof-shell-process-name proof-shell-buffer-name)
+      (message 
+       (format "Starting %s process... done." proof-shell-process-name)))))
+  
+
+(defun proof-spawn-process (prog-name process-name buffer-name)
+  "Start a new shell in a new buffer"
+
+  (set-buffer
+   (let ((prog-name-list (string-to-list prog-name " ")))
+     (apply 'make-comint 
+	    (append (list process-name 
+			  (car prog-name-list) nil)
+		    (cdr prog-name-list)))))
+
+  (erase-buffer)
+  (funcall proof-shell-mode-is)
+  (setq comint-prompt-regexp proof-shell-prompt-pattern)
+  (setq comint-scroll-to-bottom-on-output t)
+  (setq comint-input-sender 'proof-input-sender)
+  (and running-emacs19 (setq comint-scroll-show-maximum-output t))
+
+  (run-hooks 'proof-shell-pre-display-hook)
+  (proof-display-buffer buffer-name)
+  (set-buffer buffer-name)
+  (run-hooks 'proof-shell-post-display-hook)
+  )
+
+(defun proof-shell-exit ()
+  "Exit the PROOF process
+
+  Runs proof-shell-exit-hook if non nil"
+
+  (interactive)
+  (save-excursion
+    (let ((buffer (proof-shell-buffer)))
+      (and buffer
+	   (progn
+	     (save-excursion
+	       (set-buffer buffer)
+	       (comint-send-eof))
+	     (kill-buffer buffer)
+	     (run-hooks 'proof-shell-exit-hook)
+
+             ;;it is important that the hooks are
+	     ;;run after the buffer has been killed. In the reverse
+	     ;;order e.g., intall-shell-fonts causes problems and it
+	     ;;is impossilbe to restart the PROOF shell
+
+	     (message 
+	      (format "%s process terminated." proof-shell-process-name)))))))
+
+(defun proof-interrupt-subjob ()
+  "Send an interrupt signal to the PROOF process."
+  (interactive) (proof-simple-send "\C-q\C-c" t))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;          Active terminator minor mode                            ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defvar proof-active-terminator-minor-mode nil)
+(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
+is positive.
+
+If Active terminator mode is enabled, a terminator will process the
+current command."
+
+ (interactive "P")
+ 
+;; has this minor mode been registered as such?
+  (or (assq 'proof-active-terminator-minor-mode minor-mode-alist)
+      (setq minor-mode-alist
+            (append minor-mode-alist
+                    (list '(proof-active-terminator-minor-mode " ;")))))
+
+ (setq proof-active-terminator-minor-mode
+        (if (null arg) (not proof-active-terminator-minor-mode)
+          (> (prefix-numeric-value arg) 0)))
+   (if (fboundp 'redraw-modeline) (redraw-modeline) (force-mode-line-update)))
+
+(defun proof-active-terminator ()
+  (interactive)
+  (if proof-active-terminator-minor-mode 
+      (proof-process-active-terminator)
+    (self-insert-command 1)))
+    
+(defun proof-process-active-terminator ()
+  "Process an active terminator key-press"  
+
+  (interactive)
+  (let (start)
+    (and (re-search-backward "[^ ]" nil t)
+	 (not (char-equal (following-char) proof-terminal-char)) 
+	 (forward-char))
+    (save-excursion
+      (setq start (proof-find-start-of-command)))
+    (if (not start)
+	 (self-insert-command 1)
+       (if (> start (point))
+	   (setq start (point)))
+       (run-hooks 'lego-shell-safe-send-hook)
+       (proof-simulate-send-region start (point) t)
+       (if (char-equal proof-terminal-char (following-char))
+	   (forward-char)
+	 (self-insert-command 1)))))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; font lock faces: declarations, errors, tacticals                 ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defvar font-lock-declaration-name-face 
+(progn 
+  (cond ((x-display-color-p)
+	 ;notice that device-class does not exist in Emacs 19.30
+
+	 (copy-face 'bold 'font-lock-declaration-name-face)
+
+	 ;; Emacs 19.28 compiles this down to
+	 ;; internal-set-face-1. This is not compatible with XEmacs
+	 (dont-compile
+	   (set-face-foreground
+	    'font-lock-declaration-name-face "chocolate")))
+	(t (copy-face 'bold-italic 'font-lock-declaration-name-face)))
+  (if running-emacs19
+      (setq font-lock-declaration-name-face
+	    (face-name 'font-lock-declaration-name-face)))))
+
+(defvar font-lock-tacticals-name-face
+(if (x-display-color-p)
+    (let ((face (make-face 'font-lock-tacticals-name-face)))
+      (dont-compile
+	(set-face-foreground face
+			     "MediumOrchid3"))
+      face)
+  (copy-face 'bold 'font-lock-tacticals-name-face)))
+
+(defvar font-lock-error-face
+(if (x-display-color-p)
+    (let ((face (make-face 'font-lock-error-face)))
+      (dont-compile
+	(set-face-foreground face
+			     "red"))
+      face)
+  (copy-face 'bold 'font-lock-error-face)))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Proof mode configuration                                         ;;
+;; Eventually there will be some functionality here common to both  ;;
+;; coq and lego. But for the moment, they're just mode shells.      ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+
+(define-derived-mode proof-mode fundamental-mode 
+  "Proof" "Proof mode - not standalone"
+  ())
+
+
+(define-derived-mode proof-shell-mode comint-mode 
+  "proof-shell" "Proof shell mode - not standalone"
+  ())
+
+;; the following callback is an irritating hack - there should be some
+;; elegant mechanism for computing constants after the child has
+;; configured.
+
+(defun proof-mode-child-config-done () 
+
+  (setq proof-shell-buffer-name (concat "*" proof-shell-process-name "*"))
+
+;; calculate some strings and regexps for searching
+
+  (setq proof-terminal-string (char-to-string proof-terminal-char))
+
+  (make-local-variable 'comment-start)
+  (setq comment-start (concat proof-comment-start " "))
+  (make-local-variable 'comment-end)
+  (setq comment-end (concat " " proof-comment-end))
+  (make-local-variable 'comment-start-skip)
+  (setq comment-start-skip 
+    (concat (regexp-quote proof-comment-start) "+\\s_?"))
+
+  (setq proof-re-end-of-cmd (concat "\\s_*" proof-terminal-string "\\s_*\\\'"))
+  (setq proof-re-term-or-comment 
+	(concat proof-terminal-string "\\|" (regexp-quote proof-comment-start)
+		"\\|" (regexp-quote proof-comment-end)))
+  )
+
+
+(provide 'proof)