diff options
| author | Pierre Courtieu | 2007-11-07 11:43:33 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2007-11-07 11:43:33 +0000 |
| commit | 470bfe858d58f293fa737c22973fe8ce07e6bf71 (patch) | |
| tree | 7915ecadb1e881dbd4fe167b8550a705405b4be4 /coq | |
| parent | 6f8ade23551add38a07a62033993f85f4efe3872 (diff) | |
Menu are now correctly sorted.
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-db.el | 4 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 1 |
2 files changed, 4 insertions, 1 deletions
diff --git a/coq/coq-db.el b/coq/coq-db.el index 9c472f91..b29c8c57 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -157,12 +157,14 @@ for DB structure." " ... " (car-safe (car-safe (nthcdr (- size 1) db))))) +(defun coq-sort-menu-entries (menu) + (sort menu '(lambda (x y) (string< (downcase (elt x 0)) (downcase (elt y 0)))))) (defun coq-build-menu-from-db (db &optional size) "Take a keyword database DB and return a list of insertion menus for them. Submenus contain SIZE entries (default 30). See `coq-syntax-db' for DB structure." - (let* ((l db) (res + (let* ((l (coq-sort-menu-entries db)) (res ()) (wdth (+ 2 (max-length-db coq-tactics-db))) (sz (or size 30)) (lgth (length l))) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 8e84b18d..5bdb08d0 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -451,6 +451,7 @@ so for the following reasons: ("Identity Coercion" nil "Identity Coercion #." t "Identity\\s-+Coercion") ("Implicit Arguments Off" nil "Implicit Arguments Off." t "Implicit\\s-+Arguments\\s-+Off") ("Implicit Arguments On" nil "Implicit Arguments On." t "Implicit\\s-+Arguments\\s-+On") + ("Implicit Arguments" nil "Implicit Arguments # [#]." t "Implicit\\s-+Arguments") ("Import" nil "Import #." t "Import") ("Infix" "inf" "Infix \"#\" := # (at level #) : @{scope}." t "Infix") ("Inspect" nil "Inspect #." nil "Inspect") |