blob: f4c4b033d32c4ebf63b7bafd89b26da5fd8bb0e1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
|
;; coq.el --- Coq mode editing commands for Emacs
;;
;; Jean-Christophe Filliatre, march 1995
;; Honteusement pompé de caml.el, Xavier Leroy, july 1993.
;;
;; modified by Marco Maggesi <maggesi@math.unifi.it> for coq-inferior
; compatibility code for proofgeneral files
(require 'coq-font-lock)
; ProofGeneral files. remember to remove coq version tests in
; coq-syntax.el
(require 'coq-syntax)
(defvar coq-mode-map nil
"Keymap used in Coq mode.")
(if coq-mode-map
()
(setq coq-mode-map (make-sparse-keymap))
(define-key coq-mode-map "\t" 'coq-indent-command)
(define-key coq-mode-map "\M-\t" 'coq-unindent-command)
(define-key coq-mode-map "\C-c\C-c" 'compile)
)
(defvar coq-mode-syntax-table nil
"Syntax table in use in Coq mode buffers.")
(if coq-mode-syntax-table
()
(setq coq-mode-syntax-table (make-syntax-table))
; ( is first character of comment start
(modify-syntax-entry ?\( "()1" coq-mode-syntax-table)
; * is second character of comment start,
; and first character of comment end
(modify-syntax-entry ?* ". 23" coq-mode-syntax-table)
; ) is last character of comment end
(modify-syntax-entry ?\) ")(4" coq-mode-syntax-table)
; quote is a string-like delimiter (for character literals)
(modify-syntax-entry ?' "\"" coq-mode-syntax-table)
; quote is part of words
(modify-syntax-entry ?' "w" coq-mode-syntax-table)
)
(defvar coq-mode-indentation 2
"*Indentation for each extra tab in Coq mode.")
(defun coq-mode-variables ()
(set-syntax-table coq-mode-syntax-table)
(make-local-variable 'paragraph-start)
(setq paragraph-start (concat "^$\\|" page-delimiter))
(make-local-variable 'paragraph-separate)
(setq paragraph-separate paragraph-start)
(make-local-variable 'paragraph-ignore-fill-prefix)
(setq paragraph-ignore-fill-prefix t)
(make-local-variable 'require-final-newline)
(setq require-final-newline t)
(make-local-variable 'comment-start)
(setq comment-start "(* ")
(make-local-variable 'comment-end)
(setq comment-end " *)")
(make-local-variable 'comment-column)
(setq comment-column 40)
(make-local-variable 'comment-start-skip)
(setq comment-start-skip "(\\*+ *")
(make-local-variable 'parse-sexp-ignore-comments)
(setq parse-sexp-ignore-comments nil)
(make-local-variable 'indent-line-function)
(setq indent-line-function 'coq-indent-command)
(make-local-variable 'font-lock-keywords)
(setq font-lock-defaults '(coq-font-lock-keywords-1)))
;;; The major mode
(defun coq-mode ()
"Major mode for editing Coq code.
Tab at the beginning of a line indents this line like the line above.
Extra tabs increase the indentation level.
\\{coq-mode-map}
The variable coq-mode-indentation indicates how many spaces are
inserted for each indentation level."
(interactive)
(kill-all-local-variables)
(setq major-mode 'coq-mode)
(setq mode-name "coq")
(use-local-map coq-mode-map)
(coq-mode-variables)
(run-hooks 'coq-mode-hook))
;;; Indentation stuff
(defun coq-in-indentation ()
"Tests whether all characters between beginning of line and point
are blanks."
(save-excursion
(skip-chars-backward " \t")
(bolp)))
(defun coq-indent-command ()
"Indent the current line in Coq mode.
When the point is at the beginning of an empty line, indent this line like
the line above.
When the point is at the beginning of an indented line
\(i.e. all characters between beginning of line and point are blanks\),
increase the indentation by one level.
The indentation size is given by the variable coq-mode-indentation.
In all other cases, insert a tabulation (using insert-tab)."
(interactive)
(let* ((begline
(save-excursion
(beginning-of-line)
(point)))
(current-offset
(- (point) begline))
(previous-indentation
(save-excursion
(if (eq (forward-line -1) 0) (current-indentation) 0))))
(cond ((and (bolp)
(looking-at "[ \t]*$")
(> previous-indentation 0))
(indent-to previous-indentation))
((coq-in-indentation)
(indent-to (+ current-offset coq-mode-indentation)))
(t
(insert-tab)))))
(defun coq-unindent-command ()
"Decrease indentation by one level in Coq mode.
Works only if the point is at the beginning of an indented line
\(i.e. all characters between beginning of line and point are blanks\).
Does nothing otherwise."
(interactive)
(let* ((begline
(save-excursion
(beginning-of-line)
(point)))
(current-offset
(- (point) begline)))
(if (and (>= current-offset coq-mode-indentation)
(coq-in-indentation))
(backward-delete-char-untabify coq-mode-indentation))))
;;; coq.el ends here
(provide 'coq)
|
