;;; 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 coq.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 "coq" "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 'coq)
(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)))
(next-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)