diff options
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-indent.el | 11 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 24 | ||||
| -rw-r--r-- | coq/coq.el | 149 | ||||
| -rw-r--r-- | coq/example-tokens.v (renamed from coq/example-x-symbols.v) | 0 | ||||
| -rw-r--r-- | coq/x-symbol-coq.el | 493 |
5 files changed, 78 insertions, 599 deletions
diff --git a/coq/coq-indent.el b/coq/coq-indent.el index 6bd41349..3258ebe3 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -161,7 +161,6 @@ comment, return nil and does not move the point." (if (= prevpos init) nil prevpos))) ; generic function is wrong when the point in between ( and * -; moreover xemacs does not deal with nested comments (defun coq-looking-at-syntactic-context () "See `proof-looking-at-syntactic-context'. Use this one for coq instead of the generic one." @@ -245,16 +244,6 @@ return nil." (if (< direction 0) (coq-find-command-end-backward) (coq-find-command-end-forward))) -;; This one to deal with nested comments in xemacs -(defun coq-parse-function () - (skip-chars-forward " \n\t") - (forward-char 1) - (if (coq-find-comment-end) - 'comment - (when (coq-find-command-end-forward) - (forward-char 1) - 'cmd))) - (defun coq-find-current-start () "Move to the start of command at point. The point is put exactly after the end of previous command, or at the (point-min if diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 27b63888..5d5d6883 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -68,7 +68,8 @@ (coq-version-is-V8 (setq coq-version-is-V8-0 nil coq-version-is-V8-1 t) (message v80)) (t;; otherwise do coqtop -v and see which version we have - (let* ((str (shell-command-to-string (concat "cd ~; " coq-prog-name " -v"))) + (let* ((default-directory (expand-file-name "~/")) + (str (shell-command-to-string (concat coq-prog-name " -v"))) ;; this match sets match-string below (ver (string-match "version v?\\([.0-9]*\\)" str))) (message str) @@ -982,9 +983,9 @@ Used by `coq-goal-command-p'" ;; (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^(.]*:\\|.*)[^(.]*:=\\)")) ;;"\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\>" (defvar coq-font-lock-keywords-1 - (append - coq-font-lock-terms - (list + (append + coq-font-lock-terms + (list (cons (proof-ids-to-regexp coq-solve-tactics) 'coq-solve-tactics-face) (cons (proof-ids-to-regexp coq-keywords) 'font-lock-keyword-face) (cons (proof-ids-to-regexp coq-reserved) 'font-lock-type-face) @@ -999,8 +1000,8 @@ Used by `coq-goal-command-p'" (list 1 'font-lock-function-name-face t)) (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face)) - (if coq-variable-highlight-enable (list (list coq-decl-with-hole-regexp 2 'font-lock-variable-name-face))) - (list + (if coq-variable-highlight-enable (list (list coq-decl-with-hole-regexp 2 'font-lock-variable-name-face))) + (list (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face) (list coq-with-with-hole-regexp 2 'font-lock-function-name-face) (list coq-save-with-hole-regexp 2 'font-lock-function-name-face) @@ -1045,9 +1046,10 @@ Used by `coq-goal-command-p'" 1)) (append coq-keywords-decl coq-keywords-defn coq-keywords-goal))) -(provide 'coq-syntax) - ;;; coq-syntax.el ends here -; Local Variables: *** -; indent-tabs-mode: nil *** -; End: *** +;; Local Variables: *** +;; indent-tabs-mode: nil *** +;; End: *** + +(provide 'coq-syntax) +;;; coq-syntax.el ends here @@ -91,13 +91,8 @@ Set to t if you want this feature." (require 'coq-syntax) (require 'coq-indent) -;; utf-8 is not yet well accepted (especially by xemacs) -;; Set to t in your .emacs to enable it. Needs to load -;; library `un-define' to work on xemacs." -;; (or (boundp 'proof-shell-unicode) (setq proof-shell-unicode nil)) -;; da: I think the default t setting now works fine, at least for me. -;; pc: 8.0 backward compliance: -(if coq-version-is-V8-0 (setq proof-shell-unicode nil)) +(if coq-version-is-V8-0 + (setq proof-shell-unicode nil)) (defcustom coq-prog-env nil "*List of environment settings d to pass to Coq process. @@ -139,8 +134,6 @@ On Windows you might need something like: ;; Configuration -(setq tags-always-exact t) ; Tags is unusable with Coq library otherwise: - (defun coq-library-directory () (let ((c (substring (shell-command-to-string "coqtop -where") 0 -1 ))) (if (string-match c "not found") @@ -676,12 +669,15 @@ happen since one of them is necessarily set to t in coq-syntax.el." (defun coq-guess-or-ask-for-string (s &optional dontguess) (let ((guess - (and (not dontguess) - (if (region-exists-p) - (buffer-substring-no-properties (region-beginning) (region-end)) - (thing-at-point 'symbol))))) - (read-string - (if guess (concat s " (default " guess "): ") (concat s " : ")) + (cond + (dontguess nil) + ((region-exists-p) + (buffer-substring-no-properties (region-beginning) (region-end))) + ((fboundp 'symbol-near-point) (symbol-near-point)) + ((fboundp 'symbol-at-point) (symbol-at-point))))) + (if (and guess (symbolp guess)) (setq guess (symbol-name guess))) + (read-string + (if guess (concat s " (default " guess "): ") (concat s ": ")) nil 'proof-minibuffer-history guess))) @@ -830,6 +826,8 @@ This is specific to `coq-mode'." ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defun coq-mode-config () + ;; Tags is unusable with Coq library otherwise: + (set (make-local-variable 'tags-always-exact) t) ;; Coq error messages are thrown off by TAB chars. (set (make-local-variable 'indent-tabs-mode) nil) (setq proof-terminal-char ?\.) @@ -863,10 +861,6 @@ This is specific to `coq-mode'." pg-topterm-goalhyplit-fn 'coq-goal-hyp proof-state-preserving-p 'coq-state-preserving-p) - ;; This one to deal with nested comments in xemacs - (if (featurep 'xemacs) - (setq proof-script-parse-function 'coq-parse-function)) - (setq proof-shell-indentifier-under-mouse-cmd "Check %s.") (setq proof-save-command-regexp coq-save-command-regexp @@ -902,11 +896,10 @@ This is specific to `coq-mode'." proof-shell-stop-silent-cmd "Unset Silent. ") (coq-init-syntax-table) - ;(setq comment-quote-nested nil) ;; we can cope with nested comments (set (make-local-variable 'comment-quote-nested) nil) ;; we can cope with nested comments ;; font-lock - (setq font-lock-keywords coq-font-lock-keywords-1) + (setq proof-script-font-lock-keywords coq-font-lock-keywords-1) ;;holes (holes-mode 1) @@ -926,7 +919,6 @@ This is specific to `coq-mode'." ("coq" . coq-tags)) tag-table-alist))) -; (setq blink-matching-paren-dont-ignore-comments t) (set (make-local-variable 'blink-matching-paren-dont-ignore-comments) t) ;; multiple file handling @@ -1010,7 +1002,8 @@ To be used in `proof-shell-process-output-system-specific'." ) (coq-init-syntax-table) - (setq font-lock-keywords coq-font-lock-keywords-1) + ; da: suggest no fontification in shell + ;(setq font-lock-defaults 'coq-font-lock-keywords-1) (holes-mode 1) (proof-shell-config-done) ) @@ -1019,12 +1012,14 @@ To be used in `proof-shell-process-output-system-specific'." (setq pg-goals-change-goal "Show %s . ") (setq pg-goals-error-regexp coq-error-regexp) (coq-init-syntax-table) - (setq font-lock-keywords coq-font-lock-keywords-1) + (setq proof-goals-font-lock-keywords coq-font-lock-keywords-1) (proof-goals-config-done)) (defun coq-response-config () (coq-init-syntax-table) - (setq font-lock-keywords coq-font-lock-keywords-1) + (setq proof-response-font-lock-keywords coq-font-lock-keywords-1) + ;; The line wrapping in this buffer just seems to make it less readable. + (setq truncate-lines t) (proof-response-config-done)) @@ -1084,6 +1079,11 @@ To be used in `proof-shell-process-output-system-specific'." "*Whether to display timing information for each command." :type 'boolean) +(defpacustom undo-limit 100 + "*Depth of undo history." + :type 'integer + :setting "Set Undo %i . ") + (defpacustom auto-compile-vos nil "Whether to automatically compile vos and track dependencies." :type 'boolean) @@ -1481,13 +1481,14 @@ be asked to the user." ;; I don't use proof-shell-last-ouput here since it is not always set to the -;; really last ouptut (specially when a *tactic* gives an error) instead I go +;; really last output (specially when a *tactic* gives an error) instead I go ;; directly to the response buffer. This allows also to clean the response ;; buffer (better to only scroll it?) (defun coq-get-last-error-location (&optional parseresp clean) - "Return location information on last error sent by coq. Return a two -elements list (pos lgth) if successful, nil otherwise. pos is the number of -characters preceding the underlined expression, and lgth is its length. + "Return location information on last error sent by coq. +Return a two elements list (POS LEN) if successful, nil otherwise. +POS is the number of characters preceding the underlined expression, +and LEN is its length. Coq error message must be like this: \" @@ -1502,20 +1503,33 @@ If PARSERESP is nil, don't really parse response buffer but take the value of If PARSERESP and CLEAN are non-nil, delete the error location from the response buffer." (if (not parseresp) last-coq-error-location - (save-excursion - ;; proof-shell-handle-error-or-interrupt-hook is called from shell buffer - (set-buffer proof-response-buffer) - (goto-char (point-max)) - (let* ((mtch (re-search-backward "\n>[^\n]+\n> \\( *\\)\\(\\^+\\)\n" nil 'dummy)) - (pos (and mtch (length (match-string 1)))) - (lgth (and (length (match-string 2)))) - (res (list pos lgth))) - ;; clean the response buffer from ultra-ugly underlined command line - ;; parsed above. Don't kill the first \n - (when (and clean mtch) (delete-region (+ mtch 1) (match-end 0))) - (when mtch - (setq last-coq-error-location res) - res))))) + ;; proof-shell-handle-error-or-interrupt-hook is called from shell buffer + (with-current-buffer proof-response-buffer + (goto-char (point-max)) + (when (re-search-backward "\n> \\(.*\\)\n> \\( *\\)\\(\\^+\\)\n" nil t) + (let ((text (match-string 1)) + (pos (length (match-string 2))) + (len (length (match-string 3)))) + ;; clean the response buffer from ultra-ugly underlined command line + ;; parsed above. Don't kill the first \n + (when clean (delete-region (+ (match-beginning 0) 1) (match-end 0))) + (when proof-shell-unicode + ;; `pos' and `len' are actually specified in bytes, apparently. + ;; So let's convert them, assuming the encoding used is utf-8. + ;; Presumably in Emacs-23 we could use `string-bytes' for that + ;; since the internal encoding happens to use utf-8 as well. + (let ((bytes (encode-coding-string text 'utf-8-unix))) + ;; Check that pos&len make sense in `bytes', if not give up. + (when (>= (length bytes) (+ pos len)) + ;; We assume here that `text' is a single line and use \n as + ;; a marker so we can find it back after decoding. + (setq bytes (concat (substring bytes 0 pos) + "\n" (substring bytes pos (+ pos len)))) + (let ((chars (decode-coding-string bytes 'utf-8-unix))) + (setq pos (string-match "\n" chars)) + (setq len (- (length chars) pos 1)))))) + (setq last-coq-error-location (list pos len))))))) + (defun coq-highlight-error (&optional parseresp clean) "Parses the last coq output looking at an error message. Highlight the text @@ -1540,36 +1554,6 @@ buffer." (set-buffer proof-script-buffer) (goto-char (+ (proof-locked-end) 1)) (coq-find-real-start) - ;; Here start som ugly code to adapt pos and lgth to x-symbol - (when (and (boundp 'x-symbol-mode) x-symbol-mode) - (let* - ((comstart (point)) - (comend (coq-find-command-end-forward)) - (reg1 100) (reg2 101) errpoint - ;(x-symbol-encode-string (coq-command-at-point) (proof-script-buffer))) -; (s2 (substring s 0 pos)) -; (s3 (x-symbol-decode)) - ) - ; remove x-symbols - (x-symbol-encode comstart comend) - ;; update comend - (setq comend (progn (goto-char comstart) (coq-find-command-end-forward)) ) - ;; go to error start and put register at start and end of error - (goto-char comstart) (forward-char pos) - (point-to-register reg1) - (forward-char lgth) - (point-to-register reg2) - ;; put symbols back, registers are moved accordingly - (x-symbol-decode-recode comstart comend) - (register-to-point reg1) - (setq errpoint (point)) - ;; adapt pos - (setq pos (- (point) comstart)) - (register-to-point reg2) - ;; adapt lgth - (setq lgth (- (point) errpoint)) - ;; go back at command start - (goto-char comstart))) ;(setq legth ??)) ; coq error positions are in byte, not in chars, so translate ; for utf-8 error message @@ -1579,9 +1563,9 @@ buffer." (byte-to-position (+ (position-bytes (point)) lgth)))) (sp (span-make start (point)))) (set-span-face sp 'proof-warning-face) - (ignore-errors (sit-for 20)) ; errors here would skip the next delete - (span-delete sp)))))) - + (unwind-protect + (sit-for 20) + (span-delete sp))))))) (defvar coq-allow-highlight-error t) @@ -1590,9 +1574,8 @@ buffer." ;; `proof-shell-insert-hook', but not by ;; `proof-shell-handle-error-or-interrupt-hook' (defun coq-decide-highlight-error () - (if (eq action 'proof-done-invisible) - (setq coq-allow-highlight-error nil) - (setq coq-allow-highlight-error t))) + (setq coq-allow-highlight-error + (not (eq action 'proof-done-invisible)))) (defun coq-highlight-error-hook () (if coq-allow-highlight-error (coq-highlight-error t t))) @@ -1607,12 +1590,10 @@ buffer." ;; goal (defun first-word-of-buffer () "Get the first word of a buffer." - (save-excursion + (save-excursion (goto-char (point-min)) - (let ((debut (point))) - (forward-word 1) - (substring (buffer-string) (- debut 1) (- (point) 1)))) - ) + (buffer-substring (point) + (progn (forward-word 1) (point))))) (defun coq-show-first-goal () diff --git a/coq/example-x-symbols.v b/coq/example-tokens.v index f890eab6..f890eab6 100644 --- a/coq/example-x-symbols.v +++ b/coq/example-tokens.v diff --git a/coq/x-symbol-coq.el b/coq/x-symbol-coq.el deleted file mode 100644 index c9abbcc8..00000000 --- a/coq/x-symbol-coq.el +++ /dev/null @@ -1,493 +0,0 @@ -;; x-symbol-coq.el -;; -;; Author: Pierre Courtieu -;; Maintainer: Pierre Courtieu -;; License GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; Directly inspired from x-symbol-isabelle.el of ProofGeneral by -;; Markus Wenzel, Christoph Wedler, David Aspinall. -;; -;; $Id$ -;; -;; NB: This file is part of the Proof General distribution. -;; - -(eval-when-compile - (require 'proof-utils) ; to properly compile 'proof-ass' - (require 'cl)) ; to properly compile 'block' - -(defvar x-symbol-coq-required-fonts nil) - -;;;=========================================================================== -;;; General language accesses, see `x-symbol-language-access-alist' -;;;=========================================================================== - -;; NB da: these next two are also set in proof-x-symbol.el, but -;; it would be handy to be able to use this file away from PG. -(defvar x-symbol-coq-name "Coq Symbol") -(defvar x-symbol-coq-modeline-name "coq") - -(defcustom x-symbol-coq-header-groups-alist nil - "*If non-nil, used in isasym specific grid/menu. -See `x-symbol-header-groups-alist'." - :group 'x-symbol-coq - :group 'x-symbol-input-init - :type 'x-symbol-headers) - -(defcustom x-symbol-coq-electric-ignore nil -;; "[:'][A-Za-z]\\|<=\\|\\[\\[\\|\\]\\]\\|~=" - "*Additional Coq version of `x-symbol-electric-ignore'." - :group 'x-symbol-coq - :group 'x-symbol-input-control - :type 'x-symbol-function-or-regexp) - -(defvar x-symbol-coq-required-fonts nil - "List of features providing fonts for language `coq'.") - -(defvar x-symbol-coq-extra-menu-items nil - "Extra menu entries for language `coq'.") - - -(defvar x-symbol-coq-token-grammar - (x-symbol-make-grammar - :encode-spec '(((id . "[a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]")) . - ((id . "[a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]"))) - :decode-spec nil - ;; decode-spec seems to go with highlighting encoding?? - :decode-regexp "\\([a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)" - :token-list #'x-symbol-coq-default-token-list - :input-spec nil)) - -;(defvar x-symbol-coq-input-token-grammar -; '("\\([_'a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)" -; ((id . "[A-Za-z_0-9]") (op . "[<>!+-*/|&]")) -; (id . "[A-Za-z_0-9]") (op . "[<>!+-*/|&]")) -; "Grammar of input method Token for language `coq'.") - -(defun x-symbol-coq-default-token-list (tokens) - (mapcar - (lambda (x) - (cons x - (cond - ;; CW: where are the shapes `id' and `op' used? - ((string-match "\\`[A-Za-z_][A-Za-z_0-9]+\\'" x) - 'id) - ((string-match "\\`[<>!+-*/|&]+\\'" x) - 'op)))) - tokens)) - -(defvar x-symbol-coq-user-table nil - "User table defining Coq commands, used in `x-symbol-coq-table'.") - -(defvar x-symbol-coq-generated-data nil - "Internal.") - - -;;;=========================================================================== -;;; No image support -;;;=========================================================================== - -(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) - - -;;;=========================================================================== -;; super- and subscripts -;;;=========================================================================== - -(defcustom x-symbol-coq-subscript-matcher 'x-symbol-coq-subscript-matcher - "Function matching super-/subscripts for language `coq'. -See language access `x-symbol-LANG-subscript-matcher'." - :group 'x-symbol-coq - :type 'function) - -(defcustom x-symbol-coq-font-lock-regexp ",{\\|__\\|\\^{\\|\\^\\^" - "Regexp matching the start tag of Coq super- and subscripts." - :group 'x-symbol-coq - :type 'regexp) - -(defcustom x-symbol-coq-font-lock-limit-regexp "}\\|\n" - "Regexp matching the end of line and the end tag of Coq -spanning super- and subscripts." - :group 'x-symbol-coq - :type 'regexp) - -(defcustom x-symbol-coq-font-lock-contents-regexp ".*" - "*Regexp matching the spanning super- and subscript contents. -This regexp should match the text between the opening and closing super- -or subscript tag." - :group 'x-symbol-coq - :type 'regexp) - -(defcustom x-symbol-coq-single-char-regexp "\\>" - "Return regexp matching \<ident> or c for some char c." - :group 'x-symbol-coq - :type 'regexp) - -(defun x-symbol-coq-subscript-matcher (limit) - (block nil - (let (open-beg open-end close-end close-beg script-type) - (while (re-search-forward x-symbol-coq-font-lock-regexp limit t) - (setq open-beg (match-beginning 0) - open-end (match-end 0) - script-type (if (or (eq (char-after (- open-end 2)) ?_) - (eq (char-after (- open-end 2)) ?,)) - 'x-symbol-sub-face - 'x-symbol-sup-face)) - (if (or (eq (char-after (- open-end 1)) ?{)) ; if is spanning sup-/subscript - (when (re-search-forward x-symbol-coq-font-lock-limit-regexp - limit 'limit) - (setq close-beg (match-beginning 0) - close-end (match-end 0)) - (when - (save-excursion - (goto-char open-end) - (re-search-forward x-symbol-coq-font-lock-contents-regexp - close-beg t)) - (store-match-data (list open-beg close-end - open-beg open-end - open-end close-beg - close-beg close-end)) - (return script-type)) - (goto-char close-beg)) - (when (re-search-forward x-symbol-coq-single-char-regexp - limit 'limit) - (setq close-end (match-end 0)) - (store-match-data (list open-beg close-end - open-beg open-end - open-end close-end)) - (return script-type)) - ))))) - -(defun coq-match-subscript (limit) - (if coq-x-symbol-enable - (setq x-symbol-coq-subscript-type - (funcall x-symbol-coq-subscript-matcher limit)))) - - - -(defvar x-symbol-coq-font-lock-allowed-faces t) -;;;=========================================================================== -;;; Charsym Info -;;;=========================================================================== - -(defcustom x-symbol-coq-class-alist - '((VALID "Coq Symbol" (x-symbol-info-face)) - (INVALID "no Coq Symbol" (red x-symbol-info-face))) - "Alist for Coq's token classes displayed by info in echo area. -See `x-symbol-language-access-alist' for details." - :group 'x-symbol-texi - :group 'x-symbol-info-strings - :set 'x-symbol-set-cache-variable - :type 'x-symbol-class-info) - - -(defcustom x-symbol-coq-class-face-alist nil - "Alist for Coq's color scheme in TeXinfo's grid and info. -See `x-symbol-language-access-alist' for details." - :group 'x-symbol-coq - :group 'x-symbol-input-init - :group 'x-symbol-info-general - :set 'x-symbol-set-cache-variable - :type 'x-symbol-class-faces) - - -(defvar x-symbol-coq-font-lock-keywords nil) - -(defvar x-symbol-coq-font-lock-allowed-faces t) - -;;;=========================================================================== -;;; The tables -;;;=========================================================================== - -(defvar x-symbol-coq-case-insensitive nil) -(defvar x-symbol-coq-token-shape nil) -(defvar x-symbol-coq-input-token-ignore nil) -(defvar x-symbol-coq-token-list 'identity) - -(defvar x-symbol-coq-symbol-table ; symbols (coq font) - '((visiblespace "spacespace") - (Gamma "Gamma") - (Delta "Delta") - (Theta "Theta") - (Lambda "Lambda") - (Pi "Pi") - (Sigma "Sigma") - (Phi "Phi") - (Psi "Psi") - (Omega "Omega") - (alpha "alpha") - (beta "beta") - (gamma "gamma") - (delta "delta") - (epsilon1 "epsilon") - (zeta "zeta") - (eta "eta") - (theta "theta") - (kappa1 "kappa") - (lambda "lambda") - (mu "mu") - (nu "nu") - (xi "xi") - (pi "pi") - (rho1 "rho") - (sigma "sigma") - (tau "tau") - (phi1 "phi") - (chi "chi") - (psi "psi") - (omega "omega") - - (notsign "~") - (logicaland "/\\") - (logicalor "\\/") - (universal1 "forall") - (existential1 "exists") - (biglogicaland "And") - (ceilingleft "lceil") - (ceilingright "rceil") - (floorleft "lfloor") - (floorright "rfloor") - (bardash "|-") - (bardashdbl "|=") - (semanticsleft "lbrakk") - (semanticsright "rbrakk") - (periodcentered "cdot") -; (element "in") ; coq keyword - (element "In") - (reflexsubset "subseteq") - (intersection "inter") - (union "union") - (bigintersection "Inter") - (bigunion "Union") - (sqintersection "sqinter") - (squnion "squnion") - (bigsqintersection "Sqinter") - (bigsqunion "Squnion") - (perpendicular "False") - (dotequal "doteq") - (wrong "wrong") - (equivalence "<->") - (notequal "<>") - (propersqsubset "sqsubset") - (reflexsqsubset "sqsubseteq") - (properprec "prec") - (reflexprec "preceq") -; (propersucc "succ") - (approxequal "approx") - (similar "sim") - (simequal "simeq") - (lessequal "<=") - (coloncolon "Colon") -; (arrowleft "leftarrow") - (arrowleft "<-") - (endash "midarrow") -; (arrowright "rightarrow") ; only -> - (arrowright "->") -; (arrowdblleft "Leftarrow") -; (nil "Midarrow") -; (arrowdblright "Rightarrow") ; only => - (arrowdblright "=>") - (frown "frown") - (mapsto "mapsto") - (leadsto "leadsto") - (arrowup "up") - (arrowdown "down") - (notelement "notin") - (multiply "times") - (circleplus "oplus") - (circleminus "ominus") - (circlemultiply "otimes") - (circleslash "oslash") - (propersubset "subset") - (infinity "infinity") - (box "box") - (lozenge1 "diamond") - (circ "circ") - (bullet "bullet") - (bardbl "parallel") - (radical "surd") - (copyright "copyright"))) - -(defvar x-symbol-coq-xsymbol-table ; xsymbols - '((Xi "Xi") - (Upsilon1 "Upsilon") - (iota "iota") - (upsilon "upsilon") - (plusminus "plusminus") -; (division "div") - (longarrowright "longrightarrow") - (longarrowleft "longleftarrow") - (longarrowboth "longleftrightarrow") - (longarrowdblright "Longrightarrow") - (longarrowdblleft "Longleftarrow") - (longarrowdblboth "Longleftrightarrow") -; (brokenbar "bar") - (hyphen "hyphen") -; (macron "inverse") - (exclamdown "exclamdown") - (questiondown "questiondown") - (guillemotleft "guillemotleft") - (guillemotright "guillemotright") -; (degree "degree") - (onesuperior "onesuperior") - (onequarter "onequarter") - (twosuperior "twosuperior") - (onehalf "onehalf") - (threesuperior "threesuperior") - (threequarters "threequarters") -; (paragraph "paragraph") - (registered "registered") - (ordfeminine "ordfeminine") - (masculine "ordmasculine") -; (section "section") - (sterling "pounds") -; (yen "yen") -; (cent "cent") - (currency "currency") - (braceleft2 "lbrace") - (braceright2 "rbrace") - (top "True") - (congruent "cong") - (club "clubsuit") - (diamond "diamondsuit") - (heart "heartsuit") - (spade "spadesuit") - (arrowboth "leftrightarrow") - (greaterequal ">=") - (proportional "propto") - (partialdiff "partial") - (ellipsis "dots") - (aleph "aleph") -; (Ifraktur "Im") -; (Rfraktur "Re") -; (weierstrass "wp") - (emptyset "emptyset") - (angle "angle") - (gradient "nabla") -; (product "Prod") - (arrowdblboth "Leftrightarrow") - (arrowdblup "Uparr") - (arrowdbldown "Downarr") - (angleleft "langle") - (angleright "rangle") - (summation "Sum") - (integral "integral") - (circleintegral "ointegral") - (dagger "dagger") - (sharp "sharp") -; (star "star") - (smltriangleright "triangleright") - (triangleleft "lhd") - (triangle "triangle") - (triangleright "rhd") - (trianglelefteq "unlhd") - (trianglerighteq "unrhd") - (smltriangleleft "triangleleft") - (natural "natural") - (flat "flat") - (amalg "amalg") - (Mho "mho") - (arrowupdown "updown") - (longmapsto "longmapsto") - (arrowdblupdown "Updown") - (hookleftarrow "hookleftarrow") - (hookrightarrow "hookrightarrow") - (rightleftharpoons "rightleftharpoons") - (leftharpoondown "leftharpoondown") - (rightharpoondown "rightharpoondown") - (leftharpoonup "leftharpoonup") - (rightharpoonup "rightharpoonup") - (asym "asymp") - (minusplus "minusplus") - (bowtie "bowtie") - (centraldots "cdots") - (circledot "odot") - (propersuperset "supset") - (reflexsuperset "supseteq") - (propersqsuperset "sqsupset") - (reflexsqsuperset "sqsupseteq") - (lessless "lless") - (greatergreater "ggreater") - (unionplus "uplus") - (smile "smile") - (reflexsucc "succeq") - (dashbar "stileturn") - (biglogicalor "Or") - (bigunionplus "Uplus") - (daggerdbl "ddagger") - (bigbowtie "Join") - (booleans "bool") - (complexnums "complex") - (natnums "nat") - (rationalnums "rat") - (realnums "real") - (integers "int") - (lesssim "lesssim") - (greatersim "greatersim") - (lessapprox "lessapprox") - (greaterapprox "greaterapprox") - (definedas "triangleq") - (cataleft "lparr") - (cataright "rparr") - (bigcircledot "Odot") - (bigcirclemultiply "Otimes") - (bigcircleplus "Oplus") - (coproduct "Coprod") -; (cedilla "cedilla") -; (diaeresis "dieresis") -; (acute "acute") - (hungarumlaut "hungarumlaut") - (lozenge "lozenge") -; (smllozenge "struct") ;coq keyword - (dotlessi "index") - (euro "euro") - (zero1 "zero") - (one1 "one") - (two1 "two") - (three1 "three") - (four1 "four") - (five1 "five") - (six1 "six") - (seven1 "seven") - (eight1 "eight") - (nine1 "nine") - )) - - - -(defun x-symbol-coq-prepare-table (table) - "Builds the x-symbol coq table. -Data taken from `x-symbol-coq-user-table', `x-symbol-coq-symbol-table' -and `x-symbol-coq-xsymbol-table'." - (mapcar (lambda (entry) - (list (car entry) nil - (cadr entry))) - table)) - -(defvar x-symbol-coq-table - (x-symbol-coq-prepare-table - (append - x-symbol-coq-user-table - x-symbol-coq-symbol-table - x-symbol-coq-xsymbol-table))) - -(defcustom x-symbol-coq-auto-style - '(coq-x-symbol-enable ; MODE-ON: whether to turn on interactively - nil ;; x-symbol-coding - 'null ;; x-symbol-8bits [NEVER want it; null disables search] - nil ;; x-symbol-unique - t ;; x-symbol-subscripts - nil) ;; x-symbol-image - "Variable used to document a language access. -See documentation of `x-symbol-auto-style'." - :group 'x-symbol-coq - :group 'x-symbol-mode - :type 'x-symbol-auto-style) - - -(provide 'x-symbol-coq) - |