diff options
author | Pierre Courtieu <courtieu@lri.fr> | 2015-04-14 13:53:21 +0000 |
---|---|---|
committer | Pierre Courtieu <courtieu@lri.fr> | 2015-04-14 13:53:21 +0000 |
commit | f7434ea0d899e4a95b48a47dbc0fd84e9e4bc5b0 (patch) | |
tree | f32678cce1c77a3bac65e4057483733fe80e6aae | |
parent | 6de817881dd92175165b47c672e4ab7d9fb3e4c2 (diff) |
bold unicode biders + Fixing highlighting in goals and response buffers + cleaning.
-rw-r--r-- | coq/coq-db.el | 13 | ||||
-rw-r--r-- | coq/coq-syntax.el | 37 | ||||
-rw-r--r-- | coq/coq.el | 66 |
3 files changed, 70 insertions, 46 deletions
diff --git a/coq/coq-db.el b/coq/coq-db.el index 45f2309f..dc83c85f 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -300,13 +300,22 @@ See `coq-syntax-db' for DB structure." "Face for names of cheating tactics in proof scripts." :group 'proof-faces) +(defface coq-symbol-binder-face + '((t :inherit font-lock-type-face :bold coq-bold-unicode-binders)) + "Face for unicode binders, by default a bold version of `font-lock-type-face'." + :group 'proof-faces) + (defconst coq-solve-tactics-face 'coq-solve-tactics-face "Expression that evaluates to a face. -Required so that 'proof-solve-tactics-face is a proper facename") +Required so that 'coq-solve-tactics-face is a proper facename") (defconst coq-cheat-face 'coq-cheat-face "Expression that evaluates to a face. -Required so that 'proof-solve-tactics-face is a proper facename") +Required so that 'coq-cheat-face is a proper facename") + +(defconst coq-symbol-binder-face 'coq-symbol-binder-face + "Expression that evaluates to a face. +Required so that 'coq-symbol-binder-face is a proper facename") diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index c3ef6137..308c7619 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -183,6 +183,7 @@ so for the following reasons: ("eauto with" "eaw" "eauto with @{db}" t) ("eauto" "ea" "eauto" t "eauto") ("econstructor" "econs" "econstructor" t "econstructor") + ("edestruct" "edes" "edestruct " t "edestruct") ("eexists" "eex" "eexists" t "eexists") ("eleft" "eleft" "eleft" t "eleft") ("elim using" "elu" "elim # using #" t) @@ -563,6 +564,7 @@ so for the following reasons: ("Add Setoid" nil "Add Setoid #." t "Add\\s-+Setoid") ("Admit Obligations" "oblsadmit" "Admit Obligations." nil "Admit\\s-+Obligations") ("Arguments Scope" "argsc" "Arguments Scope @{id} [ @{_} ]" t "Arguments\\s-+Scope") + ("Arguments" "args" "Arguments @{id} : @{rule}" t "Arguments") ("Bind Scope" "bndsc" "Bind Scope @{scope} with @{type}" t "Bind\\s-+Scope") ("Canonical Structure" nil "Canonical Structure #." t "Canonical\\s-+Structure") ("Cd" nil "Cd #." nil "Cd") @@ -872,6 +874,8 @@ It is used: (coq-build-regexp-list-from-db coq-tacticals-db) "Keywords for tacticals in a Coq script.") +(defvar coq-symbol-binders "\\_<∀\\_>\\|\\_<∃\\_>\\|\\_<λ\\_>") + ;; From JF Monin: (defvar coq-reserved @@ -888,9 +892,11 @@ It is used: "Reserved keywords of Coq.") ;; FIXME: ∀ and ∃ should be followed by a space in coq syntax. +;; FIXME: actually these are not exactly reserved keywords, find +;; another classification of keywords. (defvar coq-reserved-regexp - (concat "\\<with\\s-+signature\\>\\|\\_<∀\\_>\\|\\_<∃\\_>\\|\\_<λ\\_>\\|" - (proof-ids-to-regexp coq-reserved) )) + (concat "\\<with\\s-+signature\\>\\|" + (proof-ids-to-regexp coq-reserved))) (defvar coq-state-changing-tactics (coq-build-regexp-list-from-db coq-tactics-db 'filter-state-changing)) @@ -972,22 +978,23 @@ It is used: (defconst coq-exists-regexp "\\(?:\\<exists\\>\\|\\_<∃\\_>\\)") (defvar coq-font-lock-terms - (if coq-variable-highlight-enable - (list - ;; lambda binders - (list (coq-first-abstr-regexp coq-lambda-regexp "\\(?:=>\\|:\\|,\\)") 1 'font-lock-variable-name-face) - ;; forall binder - (list (coq-first-abstr-regexp coq-forall-regexp "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face) - (list (coq-first-abstr-regexp coq-exists-regexp "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face) + (cons + (cons coq-symbol-binders 'coq-symbol-binder-face) + (if coq-variable-highlight-enable + (list + ;; lambda binders + (list (coq-first-abstr-regexp coq-lambda-regexp "\\(?:=>\\|:\\|,\\)") 1 'font-lock-variable-name-face) + ;; forall binder + (list (coq-first-abstr-regexp coq-forall-regexp "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face) + (list (coq-first-abstr-regexp coq-exists-regexp "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face) ; (list "\\<forall\\>" ; (list 0 font-lock-type-face) ; (list (concat "[^ :]\\s-*\\(" coq-ids "\\)\\s-*") nil nil ; (list 0 font-lock-variable-name-face))) - - ;; parenthesized binders - (list (coq-first-abstr-regexp "(" ":[ a-zA-Z]") 1 'font-lock-variable-name-face) - (list (coq-first-abstr-regexp "{" ":[ a-zA-Z]") 1 'font-lock-variable-name-face) - )) + ;; parenthesized binders + (list (coq-first-abstr-regexp "(" ":[ a-zA-Z]") 1 'font-lock-variable-name-face) + (list (coq-first-abstr-regexp "{" ":[ a-zA-Z]") 1 'font-lock-variable-name-face) + ))) "*Font-lock table for Coq terms.") @@ -1077,6 +1084,7 @@ It is used: (append coq-font-lock-terms (list + (cons coq-reserved-regexp 'font-lock-type-face) (cons coq-keywords-regexp 'font-lock-keyword-face) (cons coq-shell-eager-annotation-start 'proof-warning-face) (cons coq-error-regexp 'proof-error-face) @@ -1091,6 +1099,7 @@ It is used: (append coq-font-lock-terms (list + (cons coq-reserved-regexp 'font-lock-type-face) (list (concat "[?]" coq-id) 0 'proof-eager-annotation-face);; highlight evars (cons "^ \\{0,2\\}\\([^ \n:()=]\\|, \\)+ *:" 'proof-declaration-name-face) (cons (proof-regexp-alt-list-symb (list "Set" "Type" "Prop")) 'font-lock-type-face)))) @@ -726,10 +726,13 @@ Return nil if S is nil." (substring s 0 (- (length s) 1)) s)) +(defun coq-is-symbol-or-punct (c) + (or (equal (char-syntax c) ?\.) (equal (char-syntax c) ?\_))) + (defun coq-grab-punctuation-left (pos) (let ((res nil) (currpos pos)) - (while (equal (char-syntax (char-before currpos)) ?\.) + (while (coq-is-symbol-or-punct (char-before currpos)(char-before currpos)) (setq res (concat (char-to-string (char-before currpos)) res)) (setq currpos (- currpos 1))) res)) @@ -738,7 +741,7 @@ Return nil if S is nil." (defun coq-grab-punctuation-right (pos) (let ((res nil) (currpos pos)) - (while (equal (char-syntax (char-after currpos)) ?\.) + (while (coq-is-symbol-or-punct (char-after currpos)) (setq res (concat res (char-to-string (char-after currpos)))) (setq currpos (+ currpos 1))) res)) @@ -751,6 +754,8 @@ Support dot.notation.of.modules." (concat (coq-grab-punctuation-left pos) (coq-grab-punctuation-right pos))))) +(defun coq-string-starts-with-symbol (s) + (eq 0 (string-match "\\s_" symbclean))) ;; remove trailing dot if any. (defun coq-id-at-point () @@ -761,10 +766,12 @@ Support dot.notation.of.modules." ((fboundp 'symbol-near-point) (symbol-near-point)) ((fboundp 'symbol-at-point) (symbol-at-point)))) (symbclean (when symb (coq-remove-trailing-dot (symbol-name symb))))) - (when (and symb (not (zerop (length symbclean)))) symbclean)))) + (when (and symb (not (zerop (length symbclean))) + (not (coq-string-starts-with-symbol symb))) + symbclean)))) (defun coq-id-or-notation-at-point () - (or (coq-id-at-point) (coq-notation-at-position (point)))) + (or (coq-id-at-point) (concat "\"" (coq-notation-at-position (point)) "\""))) (defcustom coq-remap-mouse-1 nil @@ -814,6 +821,7 @@ Otherwise propose identifier at point if any." ((use-region-p) (buffer-substring-no-properties (region-beginning) (region-end))) (t (coq-id-or-notation-at-point))))) + (message "YOUHOU: %S" guess) (read-string (if guess (concat s " (default " guess "): ") (concat s ": ")) nil 'proof-minibuffer-history guess))) @@ -888,7 +896,7 @@ More precisely it executes SETCMD, then DO id and finally silently UNSETCMD." (concat "[ " s " ]")) (defsubst coq-put-into-double-quote-if-notation (s) - (if (equal (char-syntax (string-to-char s)) ?\.) + (if (coq-is-symbol-or-punct (string-to-char s)) (concat "\"" s "\"") s)) @@ -904,12 +912,6 @@ More precisely it executes SETCMD, then DO id and finally silently UNSETCMD." (defun coq-build-removed-patterns (l) (mapcar 'coq-build-removed-pattern l)) -(defsubst coq-put-into-double-quote-if-notation-remove-ind (s) - (let ((removed (coq-build-removed-patterns coq-removed-patterns-when-search))) - (if (equal (char-syntax (string-to-char s)) ?\.) - (apply 'concat (cons "\"" (cons s (cons "\"" removed)))) - (apply 'concat (cons s removed))))) - (defsubst coq-put-into-quotes (s) (concat "\"" s "\"")) @@ -923,7 +925,7 @@ This is specific to `coq-mode'." (defun coq-SearchConstant () (interactive) - (coq-ask-do "Search constant" "Search" nil 'coq-put-into-double-quote-if-notation)) + (coq-ask-do "Search constant" "Search")) (defun coq-SearchRewrite () (interactive) @@ -934,60 +936,60 @@ This is specific to `coq-mode'." (interactive) (coq-ask-do "SearchAbout (ex: \"eq_\" eq -bool)" - "SearchAbout" nil 'coq-put-into-double-quote-if-notation-remove-ind) + "SearchAbout") (message "use `coq-SearchAbout-all' to see constants ending with \"_ind\", \"_rec\", etc")) (defun coq-SearchAbout-all () (interactive) (coq-ask-do "SearchAbout (ex: \"eq_\" eq -bool)" - "SearchAbout" nil 'coq-put-into-double-quote-if-notation)) + "SearchAbout")) (defun coq-Print (withprintingall) "Ask for an ident and print the corresponding term. With flag Printing All if some prefix arg is given (C-u)." (interactive "P") (if withprintingall - (coq-ask-do-show-all "Print" "Print" nil 'coq-put-into-double-quote-if-notation) - (coq-ask-do "Print" "Print" nil 'coq-put-into-double-quote-if-notation))) + (coq-ask-do-show-all "Print" "Print") + (coq-ask-do "Print" "Print"))) (defun coq-Print-with-implicits () "Ask for an ident and print the corresponding term." (interactive) - (coq-ask-do-show-implicits "Print" "Print" nil 'coq-put-into-double-quote-if-notation)) + (coq-ask-do-show-implicits "Print" "Print")) (defun coq-Print-with-all () "Ask for an ident and print the corresponding term." (interactive) - (coq-ask-do-show-all "Print" "Print" nil 'coq-put-into-double-quote-if-notation)) + (coq-ask-do-show-all "Print" "Print")) (defun coq-About (withprintingall) "Ask for an ident and print information on it." (interactive "P") (if withprintingall - (coq-ask-do-show-all "About" "About" nil 'coq-put-into-double-quote-if-notation) - (coq-ask-do "About" "About" nil 'coq-put-into-double-quote-if-notation))) + (coq-ask-do-show-all "About" "About") + (coq-ask-do "About" "About"))) (defun coq-About-with-implicits () "Ask for an ident and print information on it." (interactive) - (coq-ask-do-show-implicits "About" "About" nil 'coq-put-into-double-quote-if-notation)) + (coq-ask-do-show-implicits "About" "About")) (defun coq-About-with-all () "Ask for an ident and print information on it." (interactive) - (coq-ask-do-show-all "About" "About" nil 'coq-put-into-double-quote-if-notation)) + (coq-ask-do-show-all "About" "About")) (defun coq-LocateConstant () "Locate a constant." (interactive) - (coq-ask-do "Locate" "Locate" nil 'coq-put-into-double-quote-if-notation)) + (coq-ask-do "Locate" "Locate")) (defun coq-LocateLibrary () "Locate a library." (interactive) - (coq-ask-do "Locate Library" "Locate Library" nil 'coq-put-into-double-quote-if-notation)) + (coq-ask-do "Locate Library" "Locate Library")) (defun coq-LocateNotation () "Locate a notation. Put it automatically into quotes. @@ -995,7 +997,7 @@ This is specific to `coq-mode'." (interactive) (coq-ask-do "Locate notation (ex: \'exists\' _ , _)" "Locate" - nil 'coq-put-into-double-quote-if-notation)) + )) (defun coq-set-undo-limit (undos) (proof-shell-invisible-command (format "Set Undo %s . " undos))) @@ -1016,25 +1018,25 @@ This is specific to `coq-mode'." (defun coq-Print-implicit () "Ask for an ident and print the corresponding term." (interactive) - (coq-ask-do "Print Implicit" "Print Implicit" nil 'coq-put-into-double-quote-if-notation)) + (coq-ask-do "Print Implicit" "Print Implicit")) (defun coq-Check (withprintingall) "Ask for a term and print its type. With flag Printing All if some prefix arg is given (C-u)." (interactive "P") (if withprintingall - (coq-ask-do-show-all "Check" "Check" nil 'coq-put-into-double-quote-if-notation) - (coq-ask-do "Check" "Check" nil 'coq-put-into-double-quote-if-notation))) + (coq-ask-do-show-all "Check" "Check") + (coq-ask-do "Check" "Check"))) (defun coq-Check-show-implicits () "Ask for a term and print its type." (interactive) - (coq-ask-do-show-implicits "Check" "Check" nil 'coq-put-into-double-quote-if-notation)) + (coq-ask-do-show-implicits "Check" "Check")) (defun coq-Check-show-all () "Ask for a term and print its type." (interactive) - (coq-ask-do-show-all "Check" "Check" nil 'coq-put-into-double-quote-if-notation)) + (coq-ask-do-show-all "Check" "Check")) (defun coq-get-response-string-at (&optional pt) "Go forward from PT until reaching a 'response property, and return it. @@ -2257,6 +2259,8 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (define-key coq-goals-mode-map [(control ?c)(control ?a)?h] 'coq-PrintHint) (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?q)] 'coq-query) (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?w)] 'coq-adapt-printing-width) +(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?l)] 'coq-LocateConstant) +(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?n)] 'coq-LocateNotation) (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?c)] 'coq-Check) @@ -2270,6 +2274,8 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (define-key coq-response-mode-map [(control ?c)(control ?a)?h] 'coq-PrintHint) (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?q)] 'coq-query) (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?w)] 'coq-adapt-printing-width) +(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?l)] 'coq-LocateConstant) +(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?n)] 'coq-LocateNotation) (when coq-remap-mouse-1 (define-key proof-mode-map [(control down-mouse-1)] 'coq-id-under-mouse-query) |