diff options
Diffstat (limited to 'proof.el')
-rw-r--r-- | proof.el | 490 |
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) |