diff options
-rw-r--r-- | coq/x-symbol-coq.el | 129 |
1 files changed, 25 insertions, 104 deletions
diff --git a/coq/x-symbol-coq.el b/coq/x-symbol-coq.el index d0f842d5..470f1662 100644 --- a/coq/x-symbol-coq.el +++ b/coq/x-symbol-coq.el @@ -33,7 +33,6 @@ See `x-symbol-header-groups-alist'." (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 @@ -53,16 +52,17 @@ See `x-symbol-header-groups-alist'." ;; '(x-symbol-make-grammar ...) (if (fboundp 'x-symbol-make-grammar) ;; x-symbol >=4.3 versions (x-symbol-make-grammar - :encode-spec '(((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]")) . - ((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]"))) + :encode-spec '(((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*-%!{}:|]")) . + ((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*-%!{}:|]"))) :decode-spec nil - :decode-regexp "\\([_'a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)" - :token-list #'x-symbol-coq-default-token-list))) + :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 . "[<>!+-*/|&]")) + '("\\([_'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) @@ -73,7 +73,7 @@ See `x-symbol-header-groups-alist'." ;; CW: where are the shapes `id' and `op' used? ((string-match "\\`[A-Za-z_][A-Za-z_0-9]+\\'" x) 'id) - ((string-match "\\`[<>!+-*/|&]+\\'" x) + ((string-match "\\`[-<>!+*/|&]+\\'" x) 'op)))) tokens)) @@ -109,93 +109,12 @@ See `x-symbol-header-groups-alist'." ;;;=========================================================================== ;; super- and subscripts ;;;=========================================================================== +;not implemeted yet -;; one char: \<^sup>, \<^sub>, \<^isub>, and \<^isup> -;; spanning: \<^bsup>...\<^esup> and \<^bsub>..\<^esub> - -(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 "\\\\<\\^[ib]?su[bp]>" - "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\\|\\\\<\\^esu[bp]>" - "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 "\\\\\\\\?[A-Za-z0-9_']+\\|[^\\]" - "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 (eq (char-after (- open-end 2)) ?b) - 'x-symbol-sub-face - 'x-symbol-sup-face)) - (if (eq (char-after (- open-end 5)) ?b) ; 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 (proof-ass x-symbol-enable) - (setq x-symbol-coq-subscript-type - (funcall x-symbol-coq-subscript-matcher limit)))) - -;; these are used for Coq output only. x-symbol does its own -;; setup of font-lock-keywords for the theory buffer -;; (x-symbol-coq-font-lock-keywords does not belong to language -;; access any more) -(defvar x-symbol-coq-font-lock-keywords - '((coq-match-subscript - (1 x-symbol-invisible-face t) - (2 (progn x-symbol-coq-subscript-type) prepend) - (3 x-symbol-invisible-face t t))) - "Coq font-lock keywords for super- and subscripts.") +(defvar x-symbol-coq-font-lock-keywords nil) (defvar x-symbol-coq-font-lock-allowed-faces t) - ;;;=========================================================================== ;;; Charsym Info ;;;=========================================================================== @@ -263,6 +182,7 @@ See `x-symbol-language-access-alist' for details." (chi "chi") (psi "psi") (omega "omega") + (notsign "~") (logicaland "/\\") (logicalor "\\/") @@ -273,7 +193,7 @@ See `x-symbol-language-access-alist' for details." (ceilingright "rceil") (floorleft "lfloor") (floorright "rfloor") - (bardash "turnstile") + (bardash "|-") (bardashdbl "Turnstile") (semanticsleft "lbrakk") (semanticsright "rbrakk") @@ -298,17 +218,18 @@ See `x-symbol-language-access-alist' for details." (reflexsqsubset "sqsubseteq") (properprec "prec") (reflexprec "preceq") - (propersucc "succ") +; (propersucc "succ") (approxequal "approx") (similar "sim") (simequal "simeq") - (lessequal "le") + (lessequal "<=") (coloncolon "Colon") - (arrowleft "leftarrow") +; (arrowleft "leftarrow") + (arrowleft "<-") (endash "midarrow") ; (arrowright "rightarrow") ; only -> (arrowright "->") - (arrowdblleft "Leftarrow") +; (arrowdblleft "Leftarrow") ; (nil "Midarrow") ; (arrowdblright "Rightarrow") ; only => (arrowdblright "=>") @@ -378,7 +299,7 @@ See `x-symbol-language-access-alist' for details." (heart "heartsuit") (spade "spadesuit") (arrowboth "leftrightarrow") - (greaterequal "ge") + (greaterequal ">=") (proportional "propto") (partialdiff "partial") (ellipsis "dots") @@ -512,7 +433,7 @@ See `x-symbol-language-access-alist' for details." 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-subscripts nil) ;; x-symbol-image "Variable used to document a language access. See documentation of `x-symbol-auto-style'." @@ -533,10 +454,10 @@ variable `x-symbol-auto-coding-alist' for details." ;; from x-symbol-isa.el -(setq proof-xsym-extra-modes '(coq-mode) - proof-xsym-activate-command - "print_mode := ([\"xsymbols\", \"symbols\"] @ ! print_mode);" - proof-xsym-deactivate-command - "print_mode := (! print_mode \\\\ [\"xsymbols\", \"symbols\"]);") +;(setq proof-xsym-extra-modes '(coq-mode) +; proof-xsym-activate-command +; "print_mode := ([\"xsymbols\", \"symbols\"] @ ! print_mode);" +; proof-xsym-deactivate-command +; "print_mode := (! print_mode \\\\ [\"xsymbols\", \"symbols\"]);") (provide 'x-symbol-coq) |