From 1854459fef368dfc8ca870792e7e3b065a2241c6 Mon Sep 17 00:00:00 2001 From: Stefan Monnier Date: Sat, 15 Dec 2018 20:03:43 -0500 Subject: Cosmetic cleanup of coq-smie, coq-syntax, and coq-abbrev. Fix a few more cl.el leftovers. Get rid of remaining use of iso-2022. Use SMIE unconditionally. * coq/coq-abbrev.el: Use lexical-binding. (coq-install-abbrevs): Delete, only keep the relevant contents. (proof-defstringset-fn): Remove. Fold changes into the main version. * coq/coq-indent.el (coq-find-real-start): Use forward-comment. * coq/coq-smie.el: Use lexical-binding. Assume `smie` is available. (coq--string-suffix-p): Rename from coq-string-suffix-p. Use string-suffix-p for it when available. (string-suffix-p): Never define here. Change all users to use coq--string-suffix-p instead. (coq-smie-.-deambiguate): Use forward-comment. Remove unused var `beg`. (coq-backward-token-fast-nogluing-dot-friends) (coq-forward-token-fast-nogluing-dot-friends): Remove unused var `tok-other`. (coq-smie-search-token-backward): Remove unused var `p`. (coq-smie-:=-deambiguate, coq-smie-backward-token): Prefer char-before over looking-back. (coq-smie-rules): Use `pcase` over deprecated cl's `case`. * coq/coq-syntax.el: Use lexical-binding. (coq-count-match): Rewrite so it doesn't do needless heap-allocation. (coq-module-opening-p, coq-section-command-p, coq-goal-command-str-p): Use case-fold-search rather than proof-string-match. (coq-goal-command-regexp): Forward-declare. (coq-save-command-regexp-strict): Move before first use. (coq-reserved-regexp): Use a single \_< ... \_>. (coq-detect-hyps-positions): Limit search for looking-back. * coq/coq.el: Remove SMIE declarations since SMIE is always used. (coq-use-smie): Remove, unused. (coq-smie): Always require. * generic/pg-pbrpm.el: Fix leftover cl.el uses. * generic/proof-utils.el (proof-defstringset-fn): Fix copy&paste error in the docstring, improve interactive prompt. * lib/maths-menu.el: Use utf-8 and lexical-binding. --- coq/coq-abbrev.el | 48 ++++++------------------------------------------ 1 file changed, 6 insertions(+), 42 deletions(-) (limited to 'coq/coq-abbrev.el') diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 308ca865..a15db325 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -1,9 +1,9 @@ -;;; coq-abbrev.el --- coq abbrev table and menus for ProofGeneral mode +;;; coq-abbrev.el --- coq abbrev table and menus for ProofGeneral mode -*- lexical-binding:t -*- ;; 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 2003-2018 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 @@ -68,46 +68,10 @@ ;;; The abbrev table built from keywords tables ;#s and @{..} are replaced by holes by holes-abbrev-complete -(defun coq-install-abbrevs () - "Install default abbrev table for coq if no other already is." - (if (boundp 'coq-mode-abbrev-table) - ;; da: this test will always fail. Assume bound-->non-empty - ;; (not (equal coq-mode-abbrev-table (make-abbrev-table)))) - (message "Coq abbrevs already exists, default not loaded") - (define-abbrev-table 'coq-mode-abbrev-table - (append coq-tactics-abbrev-table coq-tacticals-abbrev-table - coq-commands-abbrev-table coq-terms-abbrev-table)) - ;; if we use default coq abbrev, never ask to save it - ;; PC: fix trac #382 I comment this. But how to disable abbrev - ;; saving for coq mode only? - ;;(setq save-abbrevs nil) ; - ;; DA: how about above, just temporarily disable saving? - (message "Coq default abbrevs loaded"))) - -(unless (or noninteractive (bound-and-true-p byte-compile-current-file)) - (coq-install-abbrevs)) -;;;;; - -; Redefining this macro to change the way a string option is asked to -; the user: we pre fill the answer with current value of the option; -(defun proof-defstringset-fn (var &optional othername) - "Define a function -toggle for setting an integer customize setting VAR. -Args as for the macro `proof-defstringset', except will be evaluated." - (eval - `(defun ,(if othername othername - (intern (concat (symbol-name var) "-stringset"))) (arg) - ,(concat "Set `" (symbol-name var) "' to ARG. -This function simply uses customize-set-variable to set the variable. -It was constructed with `proof-defstringset-fn'.") -; (interactive ,(format "sValue for %s (a string, currenly %s): " -; (symbol-name var) (symbol-value var))) - (interactive (list - (read-string - (format "Value for %s (float): " - (symbol-name (quote ,var)) - (symbol-value (quote ,var))) - (symbol-value (quote ,var))))) - (customize-set-variable (quote ,var) arg)))) +(define-abbrev-table 'coq-mode-abbrev-table + (append coq-tactics-abbrev-table coq-tacticals-abbrev-table + coq-commands-abbrev-table coq-terms-abbrev-table) + "Abbrev table for Coq.") ;; The coq menu partly built from tables -- cgit v1.2.3