diff options
Diffstat (limited to 'coq/coq-db.el')
| -rw-r--r-- | coq/coq-db.el | 77 |
1 files changed, 54 insertions, 23 deletions
diff --git a/coq/coq-db.el b/coq/coq-db.el index 0d9c0a6e..cad149a2 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -1,9 +1,18 @@ -;;; coq-db.el --- coq keywords database utility functions -;; +;;; coq-db.el --- coq keywords database utility functions -*- coding: utf-8; -*- + +;; This file is part of Proof General. + +;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh +;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: Pierre Courtieu <courtieu@lri.fr> + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; + ;;; Commentary: ;; ;; We store all information on keywords (tactics or command) in big @@ -69,10 +78,10 @@ new keyword to colorize.") (defun coq-insert-from-db (db prompt &optional alwaysjump) "Ask for a keyword, with completion on keyword database DB and insert. -Insert corresponding string with holes at point. If an insertion -function is present for the keyword, call it instead. see -`coq-syntax-db' for DB structure. If ALWAYSJUMP is non nil, jump -to the first hole even if more than one." +Insert corresponding string with holes at point. If an insertion +function is present for the keyword, call it instead. See +`coq-syntax-db' for DB structure. If ALWAYSJUMP is non nil, jump to +the first hole even if more than one." (let* ((tac (completing-read (concat prompt " (TAB for completion): ") db nil nil)) (infos (cddr (assoc tac db))) @@ -87,7 +96,7 @@ to the first hole even if more than one." (defun coq-build-command-from-db (db prompt &optional preformatquery) - "Ask for a keyword, with completion on keyword database DB and send to coq. + "Ask for a keyword, with completion on keyword database DB and send to Coq. See `coq-syntax-db' for DB structure." ;; Next invocation of minibuffer (read-string below) will first recursively ;; ask for a command in db and expand it with holes. This way the cursor will @@ -133,7 +142,7 @@ regexp. See `coq-syntax-db' for DB structure." ; (color (concat "\\_<" (nth 4 hd) "\\_>"))) ; colorization string ;; TODO delete doublons (when (and color (or (not filter) (funcall filter hd))) - (setq res + (setq res (nconc res (list (concat "\\_<" color "\\_>"))))) (setq l tl))) @@ -195,8 +204,8 @@ Used by `coq-build-menu-from-db', which you should probably use instead. See (let ((menu-entry (vector ;; menu entry label - (concat menu - (if (not abbrev) "" + (concat menu + (if (not abbrev) "" (concat spaces "(" abbrev keybind-abbrev ")"))) ;;insertion function if present otherwise insert completion (if insertfn insertfn `(holes-insert-and-expand ,complt)) @@ -245,8 +254,7 @@ structure." res)) (defcustom coq-holes-minor-mode t - "*Whether to apply holes minor mode (see `holes-show-doc') in - coq mode." + "*Whether to apply holes minor mode (see `holes-show-doc') in coq mode." :type 'boolean :group 'coq) @@ -284,19 +292,20 @@ See `coq-syntax-db' for DB structure." (defface coq-solve-tactics-face (proof-face-specs (:foreground "red") ; pour les fonds clairs - (:foreground "red") ; pour les fond foncés + (:foreground "red1") ; pour les fonds foncés ()) ; pour le noir et blanc "Face for names of closing tactics in proof scripts." :group 'proof-faces) -;;A new face for cheating tactics -;; FIXMe: the background color disappear when locked region overrides it. -;; this is hard to fix without re-colorizing afterward. +;;A face for cheating tactics +;; We use :box in addition to :background because box remains visible in +;; locked-region. :reverse-video is another solution. (defface coq-cheat-face - (proof-face-specs - (:background "red") ; pour les fonds clairs - (:background "red") ; pour les fond foncés - ()) ; pour le noir et blanc + '(;(((class color) (background light)) . (:inverse-video t :foreground "red" :background "black")) + ;(((class color) (background dark)) . (:inverse-video t :foreground "red1")) + (((class color) (background light)) . (:box (:line-width -1 :color "red" :style nil) :background "red")) + (((class color) (background dark)) . (:box (:line-width -1 :color "red1" :style nil) :background "red1")) + (t . ())) ; monocolor or greyscale: no highlight "Face for names of cheating tactics in proof scripts." :group 'proof-faces) @@ -306,7 +315,7 @@ See `coq-syntax-db' for DB structure." :group 'proof-faces) (defface coq-symbol-face - '((t :inherit default-face :bold coq-bold-unicode-binders)) + '((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) @@ -320,6 +329,28 @@ See `coq-syntax-db' for DB structure." "Face used for `ltac:', `constr:', and `uconstr:' headers." :group 'proof-faces) +;; This messes columns, can't figure out why putting this face makes the overlay +;; larger than a character +;; (defface coq-button-face +;; '((t :inherit custom-button :background "dark gray")) +;; "" +;; :group 'proof-faces) + +;; (defface coq-button-face-pressed +;; '((t :inherit custom-button-pressed :background "light gray")) +;; "" +;; :group 'proof-faces) + +(defface coq-button-face + '((t . (:background "light gray"))) + "" + :group 'proof-faces) + +(defface coq-button-face-pressed + '((t . (:background "dark gray"))) + "" + :group 'proof-faces) + (defconst coq-solve-tactics-face 'coq-solve-tactics-face "Expression that evaluates to a face. Required so that 'coq-solve-tactics-face is a proper facename") |