diff options
Diffstat (limited to 'tools/inferior-coq.el')
| -rw-r--r-- | tools/inferior-coq.el | 324 |
1 files changed, 324 insertions, 0 deletions
diff --git a/tools/inferior-coq.el b/tools/inferior-coq.el new file mode 100644 index 00000000..453bd139 --- /dev/null +++ b/tools/inferior-coq.el @@ -0,0 +1,324 @@ +;;; inferior-coq.el --- Run an inferior Coq process. +;;; +;;; Copyright (C) Marco Maggesi <maggesi@math.unifi.it> +;;; Time-stamp: "2002-02-28 12:15:04 maggesi" + + +;; Emacs Lisp Archive Entry +;; Filename: inferior-coq.el +;; Version: 1.0 +;; Keywords: process coq +;; Author: Marco Maggesi <maggesi@math.unifi.it> +;; Maintainer: Marco Maggesi <maggesi@math.unifi.it> +;; Description: Run an inferior Coq process. +;; URL: http://www.math.unifi.it/~maggesi/ +;; Compatibility: Emacs20, Emacs21, XEmacs21 + +;; This is free software; you can redistribute it and/or modify it under +;; the terms of the GNU General Public License as published by the Free +;; Software Foundation; either version 2, or (at your option) any later +;; version. +;; +;; This is distributed in the hope that it will be useful, but WITHOUT +;; ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or +;; FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License +;; for more details. +;; +;; You should have received a copy of the GNU General Public License +;; along with GNU Emacs; see the file COPYING. If not, write to the +;; Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, +;; MA 02111-1307, USA. + +;;; Commentary: + +;; Coq is a proof assistant (http://coq.inria.fr/). This code run an +;; inferior Coq process and defines functions to send bits of code +;; from other buffers to the inferior process. This is a +;; customisation of comint-mode (see comint.el). For a more complex +;; and full featured Coq interface under Emacs look at Proof General +;; (http://zermelo.dcs.ed.ac.uk/~proofgen/). +;; +;; Written by Marco Maggesi <maggesi@math.unifi.it> with code heavly +;; borrowed from emacs cmuscheme.el +;; +;; Please send me bug reports, bug fixes, and extensions, so that I can +;; merge them into the master source. + +;;; Installation: + +;; You need to have gallina.el already installed (it comes with the +;; standard Coq distribution) in order to use this code. Put this +;; file somewhere in you load-path and add the following lines in your +;; "~/.emacs": +;; +;; (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) +;; (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) +;; (autoload 'run-coq "inferior-coq" "Run an inferior Coq process." t) +;; (autoload 'run-coq-other-window "inferior-coq" +;; "Run an inferior Coq process in a new window." t) +;; (autoload 'run-coq-other-frame "inferior-coq" +;; "Run an inferior Coq process in a new frame." t) + +;;; Usage: + +;; Call `M-x "run-coq'. +;; +;; Functions and key bindings (Learn more keys with `C-c C-h' or `C-h m'): +;; C-return ('M-x coq-send-line) send the current line. +;; C-c C-r (`M-x coq-send-region') send the current region. +;; C-c C-a (`M-x coq-send-abort') send the command "Abort". +;; C-c C-t (`M-x coq-send-restart') send the command "Restart". +;; C-c C-s (`M-x coq-send-show') send the command "Show". +;; C-c C-u (`M-x coq-send-undo') send the command "Undo". +;; C-c C-v (`M-x coq-check-region') run command "Check" on region. +;; C-c . (`M-x coq-come-here') Restart and send until current point. + +;;; Change Log: + +;; From -0.0 to 1.0 brought into existence. + + +(require 'gallina) +(require 'comint) + +(setq coq-program-name "coqtop") + +(defgroup inferior-coq nil + "Run a coq process in a buffer." + :group 'coq) + +(defcustom inferior-coq-mode-hook nil + "*Hook for customising inferior-coq mode." + :type 'hook + :group 'coq) + +(defvar inferior-coq-mode-map + (let ((m (make-sparse-keymap))) + (define-key m "\C-c\C-r" 'coq-send-region) + (define-key m "\C-c\C-a" 'coq-send-abort) + (define-key m "\C-c\C-t" 'coq-send-restart) + (define-key m "\C-c\C-s" 'coq-send-show) + (define-key m "\C-c\C-u" 'coq-send-undo) + (define-key m "\C-c\C-v" 'coq-check-region) + m)) + +;; Install the process communication commands in the coq-mode keymap. +(define-key coq-mode-map [(control return)] 'coq-send-line) +(define-key coq-mode-map "\C-c\C-r" 'coq-send-region) +(define-key coq-mode-map "\C-c\C-a" 'coq-send-abort) +(define-key coq-mode-map "\C-c\C-t" 'coq-send-restart) +(define-key coq-mode-map "\C-c\C-s" 'coq-send-show) +(define-key coq-mode-map "\C-c\C-u" 'coq-send-undo) +(define-key coq-mode-map "\C-c\C-v" 'coq-check-region) +(define-key coq-mode-map "\C-c." 'coq-come-here) + +(defvar coq-buffer) + +(define-derived-mode inferior-coq-mode comint-mode "Inferior Coq" + "\ +Major mode for interacting with an inferior Coq process. + +The following commands are available: +\\{inferior-coq-mode-map} + +A Coq process can be fired up with M-x run-coq. + +Customisation: Entry to this mode runs the hooks on comint-mode-hook +and inferior-coq-mode-hook (in that order). + +You can send text to the inferior Coq process from other buffers +containing Coq source. + +Functions and key bindings (Learn more keys with `C-c C-h'): + C-return ('M-x coq-send-line) send the current line. + C-c C-r (`M-x coq-send-region') send the current region. + C-c C-a (`M-x coq-send-abort') send the command \"Abort\". + C-c C-t (`M-x coq-send-restart') send the command \"Restart\". + C-c C-s (`M-x coq-send-show') send the command \"Show\". + C-c C-u (`M-x coq-send-undo') send the command \"Undo\". + C-c C-v (`M-x coq-check-region') run command \"Check\" on region. + C-c . (`M-x coq-come-here') Restart and send until current point. +" + ;; Customise in inferior-coq-mode-hook + (setq comint-prompt-regexp "^[^<]* < *") + (coq-mode-variables) + (setq mode-line-process '(":%s")) + (setq comint-input-filter (function coq-input-filter)) + (setq comint-get-old-input (function coq-get-old-input))) + +(defcustom inferior-coq-filter-regexp "\\`\\s *\\S ?\\S ?\\s *\\'" + "*Input matching this regexp are not saved on the history list. +Defaults to a regexp ignoring all inputs of 0, 1, or 2 letters." + :type 'regexp + :group 'inferior-coq) + +(defun coq-input-filter (str) + "Don't save anything matching `inferior-coq-filter-regexp'." + (not (string-match inferior-coq-filter-regexp str))) + +(defun coq-get-old-input () + "Snarf the sexp ending at point." + (save-excursion + (let ((end (point))) + (backward-sexp) + (buffer-substring (point) end)))) + +(defun coq-args-to-list (string) + (let ((where (string-match "[ \t]" string))) + (cond ((null where) (list string)) + ((not (= where 0)) + (cons (substring string 0 where) + (coq-args-to-list (substring string (+ 1 where) + (length string))))) + (t (let ((pos (string-match "[^ \t]" string))) + (if (null pos) + nil + (coq-args-to-list (substring string pos + (length string))))))))) + +;;;###autoload +(defun run-coq (cmd) + "Run an inferior Coq process, input and output via buffer *coq*. +If there is a process already running in `*coq*', switch to that buffer. +With argument, allows you to edit the command line (default is value +of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook' +\(after the `comint-mode-hook' is run). +\(Type \\[describe-mode] in the process buffer for a list of commands.)" + + (interactive (list (if current-prefix-arg + (read-string "Run Coq: " coq-program-name) + coq-program-name))) + (if (not (comint-check-proc "*coq*")) + (let ((cmdlist (coq-args-to-list cmd))) + (set-buffer (apply 'make-comint "coq" (car cmdlist) + nil (cdr cmdlist))) + (inferior-coq-mode))) + (setq coq-program-name cmd) + (setq coq-buffer "*coq*") + (switch-to-buffer "*coq*")) +;;;###autoload (add-hook 'same-window-buffer-names "*coq*") + +;;;###autoload +(defun run-coq-other-window (cmd) + "Run an inferior Coq process, input and output via buffer *coq*. +If there is a process already running in `*coq*', switch to that buffer. +With argument, allows you to edit the command line (default is value +of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook' +\(after the `comint-mode-hook' is run). +\(Type \\[describe-mode] in the process buffer for a list of commands.)" + + (interactive (list (if current-prefix-arg + (read-string "Run Coq: " coq-program-name) + coq-program-name))) + (if (not (comint-check-proc "*coq*")) + (let ((cmdlist (coq-args-to-list cmd))) + (set-buffer (apply 'make-comint "coq" (car cmdlist) + nil (cdr cmdlist))) + (inferior-coq-mode))) + (setq coq-program-name cmd) + (setq coq-buffer "*coq*") + (pop-to-buffer "*coq*")) +;;;###autoload (add-hook 'same-window-buffer-names "*coq*") + +(defun run-coq-other-frame (cmd) + "Run an inferior Coq process, input and output via buffer *coq*. +If there is a process already running in `*coq*', switch to that buffer. +With argument, allows you to edit the command line (default is value +of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook' +\(after the `comint-mode-hook' is run). +\(Type \\[describe-mode] in the process buffer for a list of commands.)" + + (interactive (list (if current-prefix-arg + (read-string "Run Coq: " coq-program-name) + coq-program-name))) + (if (not (comint-check-proc "*coq*")) + (let ((cmdlist (coq-args-to-list cmd))) + (set-buffer (apply 'make-comint "coq" (car cmdlist) + nil (cdr cmdlist))) + (inferior-coq-mode))) + (setq coq-program-name cmd) + (setq coq-buffer "*coq*") + (switch-to-buffer-other-frame "*coq*")) + +(defun switch-to-coq (eob-p) + "Switch to the coq process buffer. +With argument, position cursor at end of buffer." + (interactive "P") + (if (get-buffer coq-buffer) + (pop-to-buffer coq-buffer) + (error "No current process buffer. See variable `coq-buffer'")) + (cond (eob-p + (push-mark) + (goto-char (point-max))))) + +(defun coq-send-region (start end) + "Send the current region to the inferior Coq process." + (interactive "r") + (comint-send-region (coq-proc) start end) + (comint-send-string (coq-proc) "\n")) + +(defun coq-send-line () + "Send the current line to the Coq process." + (interactive) + (save-excursion + (end-of-line) + (let ((end (point))) + (beginning-of-line) + (coq-send-region (point) end))) + (forward-line 1)) + +(defun coq-send-abort () + "Send the command \"Abort.\" to the inferior Coq process." + (interactive) + (comint-send-string (coq-proc) "Abort.\n")) + +(defun coq-send-restart () + "Send the command \"Restart.\" to the inferior Coq process." + (interactive) + (comint-send-string (coq-proc) "Restart.\n")) + +(defun coq-send-undo () + "Reset coq to the initial state and send the region between the + beginning of file and the point." + (interactive) + (comint-send-string (coq-proc) "Undo.\n")) + +(defun coq-check-region (start end) + "Run the commmand \"Check\" on the current region." + (interactive "r") + (comint-proc-query (coq-proc) + (concat "Check " + (buffer-substring start end) + ".\n"))) + +(defun coq-send-show () + "Send the command \"Show.\" to the inferior Coq process." + (interactive) + (comint-send-string (coq-proc) "Show.\n")) + +(defun coq-come-here () + "Reset coq to the initial state and send the region between the + beginning of file and the point." + (interactive) + (comint-send-string (coq-proc) "Reset Initial.\n") + (coq-send-region 1 (point))) + +(defvar coq-buffer nil "*The current coq process buffer.") + +(defun coq-proc () + "Return the current coq process. See variable `coq-buffer'." + (let ((proc (get-buffer-process (if (eq major-mode 'inferior-coq-mode) + (current-buffer) + coq-buffer)))) + (or proc + (error "No current process. See variable `coq-buffer'")))) + +(defcustom inferior-coq-load-hook nil + "This hook is run when inferior-coq is loaded in. +This is a good place to put keybindings." + :type 'hook + :group 'inferior-coq) + +(run-hooks 'inferior-coq-load-hook) + +(provide 'inferior-coq) |