Skip to content
This repository was archived by the owner on Nov 13, 2021. It is now read-only.

Commit 4def1bc

Browse files
author
filliatr
committed
coq-inferior, by Marco Maggesi
git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@2644 85f007b7-540e-0410-9357-904b9bb8a0f7
1 parent b6c00a6 commit 4def1bc

File tree

2 files changed

+347
-17
lines changed

2 files changed

+347
-17
lines changed

‎tools/coq-inferior.el

Lines changed: 324 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,324 @@
1+
;;; inferior-coq.el --- Run an inferior Coq process.
2+
;;;
3+
;;; Copyright (C) Marco Maggesi <[email protected]>
4+
;;; Time-stamp: "2002-02-28 12:15:04 maggesi"
5+
6+
7+
;; Emacs Lisp Archive Entry
8+
;; Filename: inferior-coq.el
9+
;; Version: 1.0
10+
;; Keywords: process coq
11+
;; Author: Marco Maggesi <[email protected]>
12+
;; Maintainer: Marco Maggesi <[email protected]>
13+
;; Description: Run an inferior Coq process.
14+
;; URL: http://www.math.unifi.it/~maggesi/
15+
;; Compatibility: Emacs20, Emacs21, XEmacs21
16+
17+
;; This is free software; you can redistribute it and/or modify it under
18+
;; the terms of the GNU General Public License as published by the Free
19+
;; Software Foundation; either version 2, or (at your option) any later
20+
;; version.
21+
;;
22+
;; This is distributed in the hope that it will be useful, but WITHOUT
23+
;; ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
24+
;; FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
25+
;; for more details.
26+
;;
27+
;; You should have received a copy of the GNU General Public License
28+
;; along with GNU Emacs; see the file COPYING. If not, write to the
29+
;; Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
30+
;; MA 02111-1307, USA.
31+
32+
;;; Commentary:
33+
34+
;; Coq is a proof assistant (http://coq.inria.fr/). This code run an
35+
;; inferior Coq process and defines functions to send bits of code
36+
;; from other buffers to the inferior process. This is a
37+
;; customisation of comint-mode (see comint.el). For a more complex
38+
;; and full featured Coq interface under Emacs look at Proof General
39+
;; (http://zermelo.dcs.ed.ac.uk/~proofgen/).
40+
;;
41+
;; Written by Marco Maggesi <[email protected]> with code heavly
42+
;; borrowed from emacs cmuscheme.el
43+
;;
44+
;; Please send me bug reports, bug fixes, and extensions, so that I can
45+
;; merge them into the master source.
46+
47+
;;; Installation:
48+
49+
;; You need to have coq.el already installed (it comes with the
50+
;; standard Coq distribution) in order to use this code. Put this
51+
;; file somewhere in you load-path and add the following lines in your
52+
;; "~/.emacs":
53+
;;
54+
;; (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
55+
;; (autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t)
56+
;; (autoload 'run-coq "inferior-coq" "Run an inferior Coq process." t)
57+
;; (autoload 'run-coq-other-window "inferior-coq"
58+
;; "Run an inferior Coq process in a new window." t)
59+
;; (autoload 'run-coq-other-frame "inferior-coq"
60+
;; "Run an inferior Coq process in a new frame." t)
61+
62+
;;; Usage:
63+
64+
;; Call `M-x "run-coq'.
65+
;;
66+
;; Functions and key bindings (Learn more keys with `C-c C-h' or `C-h m'):
67+
;; C-return ('M-x coq-send-line) send the current line.
68+
;; C-c C-r (`M-x coq-send-region') send the current region.
69+
;; C-c C-a (`M-x coq-send-abort') send the command "Abort".
70+
;; C-c C-t (`M-x coq-send-restart') send the command "Restart".
71+
;; C-c C-s (`M-x coq-send-show') send the command "Show".
72+
;; C-c C-u (`M-x coq-send-undo') send the command "Undo".
73+
;; C-c C-v (`M-x coq-check-region') run command "Check" on region.
74+
;; C-c . (`M-x coq-come-here') Restart and send until current point.
75+
76+
;;; Change Log:
77+
78+
;; From -0.0 to 1.0 brought into existence.
79+
80+
81+
(require 'coq)
82+
(require 'comint)
83+
84+
(setq coq-program-name "coqtop")
85+
86+
(defgroup inferior-coq nil
87+
"Run a coq process in a buffer."
88+
:group 'coq)
89+
90+
(defcustom inferior-coq-mode-hook nil
91+
"*Hook for customising inferior-coq mode."
92+
:type 'hook
93+
:group 'coq)
94+
95+
(defvar inferior-coq-mode-map
96+
(let ((m (make-sparse-keymap)))
97+
(define-key m "\C-c\C-r" 'coq-send-region)
98+
(define-key m "\C-c\C-a" 'coq-send-abort)
99+
(define-key m "\C-c\C-t" 'coq-send-restart)
100+
(define-key m "\C-c\C-s" 'coq-send-show)
101+
(define-key m "\C-c\C-u" 'coq-send-undo)
102+
(define-key m "\C-c\C-v" 'coq-check-region)
103+
m))
104+
105+
;; Install the process communication commands in the coq-mode keymap.
106+
(define-key coq-mode-map [(control return)] 'coq-send-line)
107+
(define-key coq-mode-map "\C-c\C-r" 'coq-send-region)
108+
(define-key coq-mode-map "\C-c\C-a" 'coq-send-abort)
109+
(define-key coq-mode-map "\C-c\C-t" 'coq-send-restart)
110+
(define-key coq-mode-map "\C-c\C-s" 'coq-send-show)
111+
(define-key coq-mode-map "\C-c\C-u" 'coq-send-undo)
112+
(define-key coq-mode-map "\C-c\C-v" 'coq-check-region)
113+
(define-key coq-mode-map "\C-c." 'coq-come-here)
114+
115+
(defvar coq-buffer)
116+
117+
(define-derived-mode inferior-coq-mode comint-mode "Inferior Coq"
118+
"\
119+
Major mode for interacting with an inferior Coq process.
120+
121+
The following commands are available:
122+
\\{inferior-coq-mode-map}
123+
124+
A Coq process can be fired up with M-x run-coq.
125+
126+
Customisation: Entry to this mode runs the hooks on comint-mode-hook
127+
and inferior-coq-mode-hook (in that order).
128+
129+
You can send text to the inferior Coq process from other buffers
130+
containing Coq source.
131+
132+
Functions and key bindings (Learn more keys with `C-c C-h'):
133+
C-return ('M-x coq-send-line) send the current line.
134+
C-c C-r (`M-x coq-send-region') send the current region.
135+
C-c C-a (`M-x coq-send-abort') send the command \"Abort\".
136+
C-c C-t (`M-x coq-send-restart') send the command \"Restart\".
137+
C-c C-s (`M-x coq-send-show') send the command \"Show\".
138+
C-c C-u (`M-x coq-send-undo') send the command \"Undo\".
139+
C-c C-v (`M-x coq-check-region') run command \"Check\" on region.
140+
C-c . (`M-x coq-come-here') Restart and send until current point.
141+
"
142+
;; Customise in inferior-coq-mode-hook
143+
(setq comint-prompt-regexp "^[^<]* < *")
144+
(coq-mode-variables)
145+
(setq mode-line-process '(":%s"))
146+
(setq comint-input-filter (function coq-input-filter))
147+
(setq comint-get-old-input (function coq-get-old-input)))
148+
149+
(defcustom inferior-coq-filter-regexp "\\`\\s *\\S ?\\S ?\\s *\\'"
150+
"*Input matching this regexp are not saved on the history list.
151+
Defaults to a regexp ignoring all inputs of 0, 1, or 2 letters."
152+
:type 'regexp
153+
:group 'inferior-coq)
154+
155+
(defun coq-input-filter (str)
156+
"Don't save anything matching `inferior-coq-filter-regexp'."
157+
(not (string-match inferior-coq-filter-regexp str)))
158+
159+
(defun coq-get-old-input ()
160+
"Snarf the sexp ending at point."
161+
(save-excursion
162+
(let ((end (point)))
163+
(backward-sexp)
164+
(buffer-substring (point) end))))
165+
166+
(defun coq-args-to-list (string)
167+
(let ((where (string-match "[ \t]" string)))
168+
(cond ((null where) (list string))
169+
((not (= where 0))
170+
(cons (substring string 0 where)
171+
(coq-args-to-list (substring string (+ 1 where)
172+
(length string)))))
173+
(t (let ((pos (string-match "[^ \t]" string)))
174+
(if (null pos)
175+
nil
176+
(coq-args-to-list (substring string pos
177+
(length string)))))))))
178+
179+
;;;###autoload
180+
(defun run-coq (cmd)
181+
"Run an inferior Coq process, input and output via buffer *coq*.
182+
If there is a process already running in `*coq*', switch to that buffer.
183+
With argument, allows you to edit the command line (default is value
184+
of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook'
185+
\(after the `comint-mode-hook' is run).
186+
\(Type \\[describe-mode] in the process buffer for a list of commands.)"
187+
188+
(interactive (list (if current-prefix-arg
189+
(read-string "Run Coq: " coq-program-name)
190+
coq-program-name)))
191+
(if (not (comint-check-proc "*coq*"))
192+
(let ((cmdlist (coq-args-to-list cmd)))
193+
(set-buffer (apply 'make-comint "coq" (car cmdlist)
194+
nil (cdr cmdlist)))
195+
(inferior-coq-mode)))
196+
(setq coq-program-name cmd)
197+
(setq coq-buffer "*coq*")
198+
(switch-to-buffer "*coq*"))
199+
;;;###autoload (add-hook 'same-window-buffer-names "*coq*")
200+
201+
;;;###autoload
202+
(defun run-coq-other-window (cmd)
203+
"Run an inferior Coq process, input and output via buffer *coq*.
204+
If there is a process already running in `*coq*', switch to that buffer.
205+
With argument, allows you to edit the command line (default is value
206+
of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook'
207+
\(after the `comint-mode-hook' is run).
208+
\(Type \\[describe-mode] in the process buffer for a list of commands.)"
209+
210+
(interactive (list (if current-prefix-arg
211+
(read-string "Run Coq: " coq-program-name)
212+
coq-program-name)))
213+
(if (not (comint-check-proc "*coq*"))
214+
(let ((cmdlist (coq-args-to-list cmd)))
215+
(set-buffer (apply 'make-comint "coq" (car cmdlist)
216+
nil (cdr cmdlist)))
217+
(inferior-coq-mode)))
218+
(setq coq-program-name cmd)
219+
(setq coq-buffer "*coq*")
220+
(pop-to-buffer "*coq*"))
221+
;;;###autoload (add-hook 'same-window-buffer-names "*coq*")
222+
223+
(defun run-coq-other-frame (cmd)
224+
"Run an inferior Coq process, input and output via buffer *coq*.
225+
If there is a process already running in `*coq*', switch to that buffer.
226+
With argument, allows you to edit the command line (default is value
227+
of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook'
228+
\(after the `comint-mode-hook' is run).
229+
\(Type \\[describe-mode] in the process buffer for a list of commands.)"
230+
231+
(interactive (list (if current-prefix-arg
232+
(read-string "Run Coq: " coq-program-name)
233+
coq-program-name)))
234+
(if (not (comint-check-proc "*coq*"))
235+
(let ((cmdlist (coq-args-to-list cmd)))
236+
(set-buffer (apply 'make-comint "coq" (car cmdlist)
237+
nil (cdr cmdlist)))
238+
(inferior-coq-mode)))
239+
(setq coq-program-name cmd)
240+
(setq coq-buffer "*coq*")
241+
(switch-to-buffer-other-frame "*coq*"))
242+
243+
(defun switch-to-coq (eob-p)
244+
"Switch to the coq process buffer.
245+
With argument, position cursor at end of buffer."
246+
(interactive "P")
247+
(if (get-buffer coq-buffer)
248+
(pop-to-buffer coq-buffer)
249+
(error "No current process buffer. See variable `coq-buffer'"))
250+
(cond (eob-p
251+
(push-mark)
252+
(goto-char (point-max)))))
253+
254+
(defun coq-send-region (start end)
255+
"Send the current region to the inferior Coq process."
256+
(interactive "r")
257+
(comint-send-region (coq-proc) start end)
258+
(comint-send-string (coq-proc) "\n"))
259+
260+
(defun coq-send-line ()
261+
"Send the current line to the Coq process."
262+
(interactive)
263+
(save-excursion
264+
(end-of-line)
265+
(let ((end (point)))
266+
(beginning-of-line)
267+
(coq-send-region (point) end)))
268+
(next-line 1))
269+
270+
(defun coq-send-abort ()
271+
"Send the command \"Abort.\" to the inferior Coq process."
272+
(interactive)
273+
(comint-send-string (coq-proc) "Abort.\n"))
274+
275+
(defun coq-send-restart ()
276+
"Send the command \"Restart.\" to the inferior Coq process."
277+
(interactive)
278+
(comint-send-string (coq-proc) "Restart.\n"))
279+
280+
(defun coq-send-undo ()
281+
"Reset coq to the initial state and send the region between the
282+
beginning of file and the point."
283+
(interactive)
284+
(comint-send-string (coq-proc) "Undo.\n"))
285+
286+
(defun coq-check-region (start end)
287+
"Run the commmand \"Check\" on the current region."
288+
(interactive "r")
289+
(comint-proc-query (coq-proc)
290+
(concat "Check "
291+
(buffer-substring start end)
292+
".\n")))
293+
294+
(defun coq-send-show ()
295+
"Send the command \"Show.\" to the inferior Coq process."
296+
(interactive)
297+
(comint-send-string (coq-proc) "Show.\n"))
298+
299+
(defun coq-come-here ()
300+
"Reset coq to the initial state and send the region between the
301+
beginning of file and the point."
302+
(interactive)
303+
(comint-send-string (coq-proc) "Reset Initial.\n")
304+
(coq-send-region 1 (point)))
305+
306+
(defvar coq-buffer nil "*The current coq process buffer.")
307+
308+
(defun coq-proc ()
309+
"Return the current coq process. See variable `coq-buffer'."
310+
(let ((proc (get-buffer-process (if (eq major-mode 'inferior-coq-mode)
311+
(current-buffer)
312+
coq-buffer))))
313+
(or proc
314+
(error "No current process. See variable `coq-buffer'"))))
315+
316+
(defcustom inferior-coq-load-hook nil
317+
"This hook is run when inferior-coq is loaded in.
318+
This is a good place to put keybindings."
319+
:type 'hook
320+
:group 'inferior-coq)
321+
322+
(run-hooks 'inferior-coq-load-hook)
323+
324+
(provide 'inferior-coq)

‎tools/coq.el

Lines changed: 23 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,9 @@
11
;; coq.el --- Coq mode editing commands for Emacs
2-
2+
;;
33
;; Jean-Christophe Filliatre, march 1995
44
;; Honteusement pompé de caml.el, Xavier Leroy, july 1993.
5+
;;
6+
;; modified by Marco Maggesi <[email protected]> for coq-inferior
57

68
(defvar coq-mode-map nil
79
"Keymap used in Coq mode.")
@@ -10,6 +12,7 @@
1012
(setq coq-mode-map (make-sparse-keymap))
1113
(define-key coq-mode-map "\t" 'coq-indent-command)
1214
(define-key coq-mode-map "\M-\t" 'coq-unindent-command)
15+
(define-key coq-mode-map "\C-c\C-c" 'compile)
1316
)
1417

1518
(defvar coq-mode-syntax-table nil
@@ -33,20 +36,7 @@
3336
(defvar coq-mode-indentation 2
3437
"*Indentation for each extra tab in Coq mode.")
3538

36-
;;; The major mode
37-
38-
(defun coq-mode ()
39-
"Major mode for editing Coq code.
40-
Tab at the beginning of a line indents this line like the line above.
41-
Extra tabs increase the indentation level.
42-
\\{coq-mode-map}
43-
The variable coq-mode-indentation indicates how many spaces are
44-
inserted for each indentation level."
45-
(interactive)
46-
(kill-all-local-variables)
47-
(setq major-mode 'coq-mode)
48-
(setq mode-name "coq")
49-
(use-local-map coq-mode-map)
39+
(defun coq-mode-variables ()
5040
(set-syntax-table coq-mode-syntax-table)
5141
(make-local-variable 'paragraph-start)
5242
(setq paragraph-start (concat "^$\\|" page-delimiter))
@@ -67,7 +57,23 @@ inserted for each indentation level."
6757
(make-local-variable 'parse-sexp-ignore-comments)
6858
(setq parse-sexp-ignore-comments nil)
6959
(make-local-variable 'indent-line-function)
70-
(setq indent-line-function 'coq-indent-command)
60+
(setq indent-line-function 'coq-indent-command))
61+
62+
;;; The major mode
63+
64+
(defun coq-mode ()
65+
"Major mode for editing Coq code.
66+
Tab at the beginning of a line indents this line like the line above.
67+
Extra tabs increase the indentation level.
68+
\\{coq-mode-map}
69+
The variable coq-mode-indentation indicates how many spaces are
70+
inserted for each indentation level."
71+
(interactive)
72+
(kill-all-local-variables)
73+
(setq major-mode 'coq-mode)
74+
(setq mode-name "coq")
75+
(use-local-map coq-mode-map)
76+
(coq-mode-variables)
7177
(run-hooks 'coq-mode-hook))
7278

7379
;;; Indentation stuff
@@ -173,4 +179,4 @@ Does nothing otherwise."
173179

174180
;;; coq.el ends here
175181

176-
(provide 'coq)
182+
(provide 'coq)

0 commit comments

Comments
 (0)