blob: 164ac4a5b430143e316a3bb3fcdfccf706277284 (
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
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
|
;;; coq-abbrev.el --- coq abbrev table and menus for ProofGeneral mode
;; Copyright (C) 1994 - 1998 LFCS Edinburgh.
;; Authors: Healfdene Goguen, Pierre Courtieu
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
(require 'proof)
(require 'coq-syntax)
(defun holes-show-doc ()
(interactive)
(describe-variable 'holes-doc))
(defun coq-local-vars-list-show-doc ()
(interactive)
(describe-variable 'coq-local-vars-doc))
(defconst coq-tactics-menu
(append '("INSERT TACTICS"
["Intros (smart)" coq-insert-intros t])
(coq-build-menu-from-db coq-tactics-db)))
(defconst coq-tactics-abbrev-table
(coq-build-abbrev-table-from-db coq-tactics-db))
(defconst coq-tacticals-menu
(append '("INSERT TACTICALS"
["Intros (smart)" coq-insert-intros t])
(coq-build-menu-from-db coq-tacticals-db)))
(defconst coq-tacticals-abbrev-table
(coq-build-abbrev-table-from-db coq-tacticals-db))
(defconst coq-commands-menu
(append '("INSERT COMMAND"
["Module/Section (smart)" coq-insert-section-or-module t]
["Require (smart)" coq-insert-requires t])
(coq-build-menu-from-db coq-commands-db)))
(defconst coq-commands-abbrev-table
(coq-build-abbrev-table-from-db coq-commands-db))
(defconst coq-terms-menu
(append '("INSERT TERM"
["Match (smart)" coq-insert-match t])
(coq-build-menu-from-db coq-terms-db)))
(defconst coq-terms-abbrev-table
(coq-build-abbrev-table-from-db coq-terms-db))
;;; The abbrev table built from keywords tables
;#s and @{..} are replaced by holes by holes-abbrev-complete
(if (and (boundp 'coq-mode-abbrev-table)
(not (equal coq-mode-abbrev-table (make-abbrev-table))))
(message "Coq abbrevs already exists, default not loaded")
(message "Coq default abbrevs loaded")
(define-abbrev-table 'coq-mode-abbrev-table
(append coq-tactics-abbrev-table coq-tacticals-abbrev-table
coq-commands-abbrev-table coq-terms-abbrev-table))
;if we use default coq abbrev, never ask to save it
(setq save-abbrevs nil))
;;;;;
;; The coq menu mainly built from tables
(defpgdefault menu-entries
`(
["Print..." coq-Print t]
["Check..." coq-Check t]
["About..." coq-About t]
["insert command (interactive)" coq-insert-command t]
,coq-commands-menu
["insert term (interactive)" coq-insert-term t]
,coq-terms-menu
["insert tactic (interactive)" coq-insert-tactic t]
,coq-tactics-menu
["insert tactical (interactive)" coq-insert-tactical t]
,coq-tacticals-menu
;; da: I added Show sub menu, not sure if it's helpful, but why not.
;; FIXME: submenus should be split off here. Also, these commands
;; should only be available when a proof is open.
;; pc: I added things in the show menu and called it QUERIES
("OTHER QUERIES"
["Print Hint" coq-PrintHint t]
["Show ith goal..." coq-Show t]
["Show Tree" coq-show-tree t]
["Show Proof" coq-show-proof t]
["Show Conjectures" coq-show-conjectures t];; maybe not so useful with editing in PG?
""
["Print..." coq-Print t]
["Check..." coq-Check t]
["About..." coq-About t]
["Search..." coq-SearchConstant t]
["Search Rewrite..." coq-SearchRewrite t]
["Search About..." coq-SearchAbout t]
["Search isos/pattern..." coq-SearchIsos t]
["Locate constant..." coq-LocateConstant t]
["Locate Library..." coq-LocateLibrary t]
["Pwd" coq-Pwd t]
["Inspect..." coq-Inspect t]
["Print Section..." coq-PrintSection t]
""
["Locate notation..." coq-LocateNotation t]
["Print Implicit..." coq-Print t]
["Print Scope/Visibility..." coq-PrintScope t]
)
("Holes"
;; da: I tidied this menu a bit. I personally think this "trick"
;; of inserting strings to add documentation looks like a real
;; mess in menus ... I've removed it for the three below since
;; the docs below appear in popup in messages anyway.
;;
;; "Make a hole active click on it"
;; "Disable a hole click on it (button 2)"
;; "Destroy a hole click on it (button 3)"
["Make hole at point" holes-set-make-active-hole t]
["Make selection a hole" holes-set-make-active-hole t]
["Replace active hole by selection" holes-replace-update-active-hole t]
["Jump to active hole" holes-set-point-next-hole-destroy t]
["Forget all holes in buffer" holes-clear-all-buffer-holes t]
["Tell me about holes?" holes-show-doc t]
;; look a bit better at the bottom
"Make hole with mouse: C-M-select"
"Replace hole with mouse: C-M-Shift select";; da: does this one work??
)
;; da: I also added abbrev submenu. Surprising Emacs doesn't have one?
("Abbrevs"
["Expand at point" expand-abbrev t]
["Unexpand last" unexpand-abbrev t]
["List abbrevs" list-abbrevs t]
["Edit abbrevs" edit-abbrevs t];; da: is it OK to add edit?
["Abbrev mode" abbrev-mode
:style toggle
:selected (and (boundp 'abbrev-mode) abbrev-mode)])
;; With all these submenus you have to wonder if these things belong
;; on the main menu. Are they the most often used?
["Compile" coq-Compile t]
["Set coq prog *persistently*" coq-ask-insert-coq-prog-name t]
["help on setting persistently" coq-local-vars-list-show-doc t]
))
;; da: Moved this from the main menu to the Help submenu.
;; It also appears under Holes, anyway.
(defpgdefault help-menu-entries
'(["Tell me about holes?" holes-show-doc t]
["help on setting prog name persistently for a file" coq-local-vars-list-show-doc t]))
(provide 'coq-abbrev)
|
