blob: 7d2c245e1105fcf00af958d6ccdb99c223a7120c (
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
|
;; x-symbol-coq.el
;;
;; David Aspinall, adapted from file supplied by David von Obheimb
;;
;; $Id$
;;
(defvar x-symbol-coq-symbol-table
'((perpendicular () "False" "\\<bottom>")
(top () "True" "\\<top>")
(notsign () "~" "\\<not>")
(longarrowright () "->" "\\<longrightarrow>")
(logicaland () "/\\" "\\<and>")
(logicalor () "\\/" "\\<or>")
(equivalence () "<->" "\\<equiv>")
(existential1 () "EX" "\\<exists>")
;; some naughty ones, but probably what you'd like
;; (a mess in words like "searching" !!)
(Gamma () "Gamma" "\\<Gamma>")
(Delta () "Delta" "\\<Delta>")
(Theta () "Theta" "\\<Theta>")
(Lambda () "Lambda" "\\<Lambda>")
(Pi () "Pi" "\\<Pi>")
(Sigma () "Sigma" "\\<Sigma>")
(Phi () "Phi" "\\<Phi>")
(Psi () "Psi" "\\<Psi>")
(Omega () "Omega" "\\<Omega>")
(alpha () "alpha" "\\<alpha>")
(beta () "beta" "\\<beta>")
(gamma () "gamma" "\\<gamma>")
(delta () "delta" "\\<delta>")
(epsilon1 () "epsilon" "\\<epsilon>")
(zeta () "zeta" "\\<zeta>")
(eta () "eta" "\\<eta>")
(theta1 () "theta" "\\<theta>")
(kappa1 () "kappa" "\\<kappa>")
(lambda () "lambda" "\\<lambda>")
; (mu () "mu" "\\<mu>")
; (nu () "nu" "\\<nu>")
; (xi () "xi" "\\<xi>")
; (pi () "pi" "\\<pi>")
(rho () "rho" "\\<rho>")
(sigma () "sigma" "\\<sigma>")
(tau () "tau" "\\<tau>")
(phi1 () "phi" "\\<phi>")
; (chi () "chi" "\\<chi>")
(psi () "psi" "\\<psi>")
(omega () "omega" "\\<omega>")))
;; All the stuff X-Symbol complains about
(defvar x-symbol-coq-master-directory 'ignore)
(defvar x-symbol-coq-image-searchpath '("./"))
(defvar x-symbol-coq-image-cached-dirs '("images/" "pictures/"))
(defvar x-symbol-coq-image-file-truename-alist nil)
(defvar x-symbol-coq-image-keywords nil)
(defvar x-symbol-coq-font-lock-keywords nil)
(defvar x-symbol-coq-header-groups-alist nil)
(defvar x-symbol-coq-class-alist
'((VALID "Coq Symbol" (x-symbol-info-face))
(INVALID "no Coq Symbol" (red x-symbol-info-face))))
(defvar x-symbol-coq-class-face-alist nil)
(defvar x-symbol-coq-electric-ignore nil)
(defvar x-symbol-coq-required-fonts nil)
(defvar x-symbol-coq-case-insensitive nil)
(defvar x-symbol-coq-extra-menu-items nil)
(defvar x-symbol-coq-token-grammar nil)
(defvar x-symbol-coq-input-token-grammar nil)
(defvar x-symbol-coq-generated-data nil)
;Pierre: let's try this, phi1 will be encoded, but not phia or
;philosophy. problem: blaphi will be encoded,
; other problem: false1 sholud not be encoded
;(defvar x-symbol-coq-token-shape '(?_ "[A-Za-z]+" . "[A-Za-z_]"))
(defvar x-symbol-coq-token-shape nil)
(defvar x-symbol-coq-table x-symbol-coq-symbol-table)
(defvar x-symbol-coq-user-table nil)
(defun x-symbol-coq-default-token-list (tokens) tokens)
(defvar x-symbol-coq-token-list 'x-symbol-coq-default-token-list)
(defvar x-symbol-coq-input-token-ignore nil)
;; internal stuff
(defvar x-symbol-coq-exec-specs nil)
(defvar x-symbol-coq-menu-alist nil)
(defvar x-symbol-coq-grid-alist nil)
(defvar x-symbol-coq-decode-atree nil)
(defvar x-symbol-coq-decode-alist nil)
(defvar x-symbol-coq-encode-alist nil)
(defvar x-symbol-coq-nomule-decode-exec nil)
(defvar x-symbol-coq-nomule-encode-exec nil)
(warn "Coq support for X-Symbol is highly incomplete! Please help improve it!
Send improvements to x-symbol-coq.el to proofgen@dcs.ed.ac.uk")
(provide 'x-symbol-coq)
|
