bold unicode biders + Fixing highlighting in goals and response buffers + cleaning.

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))))
diff --git a/coq/coq.el b/coq/coq.el
index b4aa039d..e8de7dde 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -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)