diff options
Diffstat (limited to 'tools/inferior-coq.el')
| -rw-r--r-- | tools/inferior-coq.el | 324 |
1 files changed, 0 insertions, 324 deletions
diff --git a/tools/inferior-coq.el b/tools/inferior-coq.el deleted file mode 100644 index 453bd139..00000000 --- a/tools/inferior-coq.el +++ /dev/null @@ -1,324 +0,0 @@ -;;; 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) |