blob: 15fb4aa730bbcbd616e24a161470346547218e9a (
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
|
--- multiple file hacking finish
--- X-sym wierdness: (1) (warning/warning) Must provide :input-spec
--- nick ideas from coq-ide: proof wizard
(also their goto point is rather nicer: suspect it uses internal
state).
--- continue plan of adding more commands to menus, etc
--- can we fontify ----- as a rule?
--- buggy indentation:
(substring (setq a (shell-command-to-string
(concat
"coqdep *.v | grep "
(file-name-nondirectory
(file-name-sans-extension fname)) ".v"
" | awk '{print $1}' | sed 's/.vo:/.v/'")))
a -- TAB here loops forever
=================================================================
;; coq-mmm.el Configure MMM mode for Coq (for LaTeX/coqdoc)
;;
;; Copyright (C) 2004 David Aspinall
;; Authors: David Aspinall <David.Aspinall@ed.ac.uk>
;; Licence: GPL
;;
;; $Id$
;;
;; Presently, we deal with several cases of (** text *).
;;
;; TODO:
;; -- complete this
;;
(require 'mmm-auto)
(defconst coq-start-latex-regexp
(concat
"\\("
(proof-ids-to-regexp
;; Perhaps section is too much? The fontification is nice but
;; section headers are a bit short to use LaTeX mode in.
(list "text" "header" ".*section"))
;; Next one is nice but hammers font lock a bit too much
;; if there are lots of -- {* short comments *}
;; "\\|\-\-" ;; NB: doesn't work with \\<--\\>
"\\)[ \t]+{\\*"))
(defconst coq-start-sml-regexp
(concat
"\\("
(proof-ids-to-regexp (list "ML" "ML_command" "ML_setup"
"typed_print_translation"))
"\\)[ \t]+{\\*"))
(mmm-add-group
'coq
`((coq-latex
:submode LaTeX-mode
:face mmm-comment-submode-face
:front ,coq-start-latex-regexp
:back "\\*}"
:insert ((?t coqtext nil @ "text {*" @ " " _ " " @ "*}" @))
:save-matches 1)
(coq-sml
:submode sml-mode
:face mmm-code-submode-face
:front ,coq-start-sml-regexp
:back "\\*}"
:insert ((?M coqml nil @ "ML_setup {*" @ " " _ " " @ "*}" @))
:save-matches 1)))
(provide 'coq-mmm)
;;; coq-mmm.el ends here
|
