aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
diff options
context:
space:
mode:
Diffstat (limited to 'coq')
-rw-r--r--coq/coq-abbrev.el48
-rw-r--r--coq/coq-autotest.el6
-rw-r--r--coq/coq-db.el16
-rw-r--r--coq/coq-indent.el2
-rw-r--r--coq/coq-par-compile.el34
-rw-r--r--coq/coq-par-test.el35
-rw-r--r--coq/coq-seq-compile.el5
-rw-r--r--coq/coq-smie.el319
-rw-r--r--coq/coq-syntax.el81
-rw-r--r--coq/coq.el131
10 files changed, 316 insertions, 361 deletions
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 <VAR>-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
diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el
index 8be4bed9..5ca66706 100644
--- a/coq/coq-autotest.el
+++ b/coq/coq-autotest.el
@@ -1,4 +1,4 @@
-;;; coq-autotest.el --- tests of Coq Proof General (in progress).
+;;; coq-autotest.el --- tests of Coq Proof General (in progress) -*- lexical-binding:t -*-
;; This file is part of Proof General.
@@ -21,7 +21,9 @@
(require 'proof-site)
(defvar coq-compile-before-require)
-(unless (bound-and-true-p byte-compile-current-file)
+;;;###autoload
+(defun coq-autotest ()
+ (interactive)
(pg-autotest start 'debug)
diff --git a/coq/coq-db.el b/coq/coq-db.el
index 36812c4c..7e59bffb 100644
--- a/coq/coq-db.el
+++ b/coq/coq-db.el
@@ -25,7 +25,7 @@
(eval-when-compile (require 'cl-lib)) ;decf
-(require 'proof-config) ; for proof-face-specs, a macro
+(require 'proof-config)
(require 'proof-syntax) ; for proof-ids-to-regexp
(require 'holes)
@@ -187,7 +187,7 @@ Used by `coq-build-menu-from-db', which you should probably use instead. See
(let ((l db) (res ()) (size lgth)
(keybind-abbrev (substitute-command-keys " \\[expand-abbrev]")))
(while (and l (> size 0))
- (let* ((hd (car l))
+ (let* ((hd (pop l))
(menu (nth 0 hd)) ; e1 = menu entry
(abbrev (nth 1 hd)) ; e2 = abbreviation
(complt (nth 2 hd)) ; e3 = completion
@@ -209,10 +209,9 @@ Used by `coq-build-menu-from-db', which you should probably use instead. See
;;insertion function if present otherwise insert completion
(if insertfn insertfn `(holes-insert-and-expand ,complt))
t)))
- (setq res (nconc res (list menu-entry)))));; append *in place*
- (setq l (cdr l))
+ (push menu-entry res)))
(cl-decf size)))
- res))
+ (nreverse res)))
(defun coq-build-title-menu (db size)
@@ -289,10 +288,9 @@ See `coq-syntax-db' for DB structure."
;;A new face for tactics which fail when they don't kill the current goal
(defface coq-solve-tactics-face
- (proof-face-specs
- (:foreground "red") ; pour les fonds clairs
- (:foreground "red1") ; pour les fonds foncés
- ()) ; pour le noir et blanc
+ `((((background light)) :foreground "red")
+ (((background dark)) :foreground "red1")
+ ()) ; pour le noir et blanc
"Face for names of closing tactics in proof scripts."
:group 'proof-faces)
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index af780251..ba4db8c3 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -523,7 +523,7 @@ the (point-min) if there is no previous command."
"Move to the start of command at point.
The point is put exactly before first non comment letter of the command."
(coq-find-current-start)
- (coq-find-not-in-comment-forward "\\S-"))
+ (forward-comment (point-max)))
(defun same-line (pt pt2)
(or (= (line-number-at-pos pt) (line-number-at-pos pt2))))
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index c6822dc5..ac2e82bf 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -35,7 +35,7 @@
;;; Code:
(defvar queueitems) ; dynamic scope in p-s-extend-queue-hook
-
+(eval-when-compile (require 'cl-lib))
(require 'coq-compile-common)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -712,7 +712,7 @@ function returns () if MODULE-ID comes from the standard library."
;; error-message)))
;; (coq-seq-display-compile-response-buffer)
(error error-message)))
- (assert (<= (length result) 1)
+ (cl-assert (<= (length result) 1)
nil "Internal error in coq-seq-map-module-id-to-obj-file")
(car-safe result)))
@@ -949,7 +949,7 @@ errors are reported with an error message."
(defun coq-par-run-vio2vo-queue ()
"Start delayed vio2vo compilation."
- (assert (not coq--last-compilation-job)
+ (cl-assert (not coq--last-compilation-job)
nil "normal compilation and vio2vo in parallel 3")
(setq coq--compile-vio2vo-in-progress t)
(setq coq--compile-vio2vo-delay-timer nil)
@@ -1011,7 +1011,7 @@ somewhere after the last require command."
(defun coq-par-add-queue-dependency (dependee dependant)
"Add queue dependency from child job DEPENDEE to parent job DEPENDANT."
- (assert (and (not (get dependant 'queue-dependant-waiting))
+ (cl-assert (and (not (get dependant 'queue-dependant-waiting))
(not (get dependee 'queue-dependant)))
nil "queue dependency cannot be added")
(put dependant 'queue-dependant-waiting t)
@@ -1202,13 +1202,13 @@ when they transition from 'waiting-queue to 'ready:
This function can safely be called for non-top-level jobs. This
function must not be called for failed jobs."
- (assert (not (get job 'failed))
+ (cl-assert (not (get job 'failed))
nil "coq-par-retire-top-level-job precondition failed")
(let ((span (get job 'require-span))
(items (get job 'queueitems)))
(when (and span coq-lock-ancestors)
(dolist (anc-job (get job 'ancestors))
- (assert (not (eq (get anc-job 'lock-state) 'unlocked))
+ (cl-assert (not (eq (get anc-job 'lock-state) 'unlocked))
nil "bad ancestor lock state")
(when (eq (get anc-job 'lock-state) 'locked)
(put anc-job 'lock-state 'asserted)
@@ -1290,7 +1290,7 @@ case, the following actions are taken:
(let ((dependant (get job 'queue-dependant)))
(if dependant
(progn
- (assert (not (eq coq--last-compilation-job job))
+ (cl-assert (not (eq coq--last-compilation-job job))
nil "coq--last-compilation-job invariant error")
(put dependant 'queue-dependant-waiting nil)
(when coq--debug-auto-compilation
@@ -1309,7 +1309,7 @@ case, the following actions are taken:
(proof-script-clear-queue-spans-on-error nil))
(proof-release-lock)
(when (eq coq-compile-quick 'quick-and-vio2vo)
- (assert (not coq--compile-vio2vo-delay-timer)
+ (cl-assert (not coq--compile-vio2vo-delay-timer)
nil "vio2vo timer set before last compilation job")
(setq coq--compile-vio2vo-delay-timer
(run-at-time coq-compile-vio2vo-delay nil
@@ -1362,7 +1362,7 @@ if it reaches 0, the next transition is triggered for DEPENDANT.
For 'file jobs this is 'waiting-dep -> 'enqueued-coqc and for
'clone jobs this 'waiting-dep -> 'waiting-queue."
;(message "%s: CPDCD with time %s" (get dependant 'name) dependee-time)
- (assert (eq (get dependant 'state) 'waiting-dep)
+ (cl-assert (eq (get dependant 'state) 'waiting-dep)
nil "wrong state of parent dependant job")
(when (coq-par-time-less (get dependant 'youngest-coqc-dependency)
dependee-time)
@@ -1371,7 +1371,7 @@ For 'file jobs this is 'waiting-dep -> 'enqueued-coqc and for
(append dependee-ancestors (get dependant 'ancestors)))
(put dependant 'coqc-dependency-count
(1- (get dependant 'coqc-dependency-count)))
- (assert (<= 0 (get dependant 'coqc-dependency-count))
+ (cl-assert (<= 0 (get dependant 'coqc-dependency-count))
nil "dependency count below zero")
(when coq--debug-auto-compilation
(message "%s: coqc dependency count down to %d"
@@ -1439,7 +1439,7 @@ This function makes the following actions.
"maybe kickoff queue")
(get job 'name)
(if dependant-alive "some" "no")))
- (assert (or (not (get job 'failed)) (not dependant-alive))
+ (cl-assert (or (not (get job 'failed)) (not dependant-alive))
nil "failed job with non-failing dependant")
(when (or (and (not dependant-alive)
(not (get job 'require-span))
@@ -1512,7 +1512,7 @@ coqdep or coqc are started for it."
(get job 'required-obj-file))))
((eq job-state 'ready)
(coq-par-start-vio2vo job))
- (t (assert nil nil "coq-par-start-task with invalid job")))))
+ (t (cl-assert nil nil "coq-par-start-task with invalid job")))))
(defun coq-par-start-jobs-until-full ()
"Start background jobs until the limit is reached."
@@ -1622,7 +1622,7 @@ Return t if job has a direct or indirect dependant that has not
failed yet and that is in a state before 'waiting-queue. Also,
return t if JOB has a dependant that is a top-level job which has
not yet failed."
- (assert (not (eq (get job 'lock-state) 'asserted))
+ (cl-assert (not (eq (get job 'lock-state) 'asserted))
nil "coq-par-ongoing-compilation precondition failed")
(cond
((get job 'failed)
@@ -1653,7 +1653,7 @@ not yet failed."
(setq res (coq-par-ongoing-compilation dep)))
res))
(t
- (assert nil nil
+ (cl-assert nil nil
"impossible ancestor state %s on job %s"
(get job 'state) (get job 'name)))))
@@ -1680,7 +1680,7 @@ Mark JOB with 'queue-failed, and, if JOB is in state
appropriate."
(unless (or (get job 'failed) (get job 'queue-failed))
(put job 'queue-failed t)
- (assert (not (eq (get job 'state) 'ready))
+ (cl-assert (not (eq (get job 'state) 'ready))
nil "coq-par-mark-queue-failing impossible state")
(when coq--debug-auto-compilation
(message "%s: mark as queue-failed, %s"
@@ -1893,7 +1893,7 @@ there is no last compilation job."
;; add the asserted items to the last compilation job
(if coq--last-compilation-job
(progn
- (assert (not (coq-par-job-is-ready coq--last-compilation-job))
+ (cl-assert (not (coq-par-job-is-ready coq--last-compilation-job))
nil "last compilation job from previous compilation ready")
(put coq--last-compilation-job 'queueitems
(nconc (get coq--last-compilation-job 'queueitems)
@@ -1979,7 +1979,7 @@ the maximal number of background compilation jobs is started."
(cancel-timer coq--compile-vio2vo-delay-timer)
(setq coq--compile-vio2vo-delay-timer nil))
(when coq--compile-vio2vo-in-progress
- (assert (not coq--last-compilation-job)
+ (cl-assert (not coq--last-compilation-job)
nil "normal compilation and vio2vo in parallel 2")
;; there are only vio2vo background processes
(coq-par-kill-all-processes)
diff --git a/coq/coq-par-test.el b/coq/coq-par-test.el
index ebc5ecd7..f2e3f01d 100644
--- a/coq/coq-par-test.el
+++ b/coq/coq-par-test.el
@@ -3,7 +3,7 @@
;; 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
@@ -31,6 +31,7 @@
;;; Code:
(require 'coq-par-compile)
+(eval-when-compile (require 'cl-lib))
(defconst coq--par-job-needs-compilation-tests
;; for documentation see the doc string following the init value
@@ -753,7 +754,7 @@ relative ages.")
(lambda (test)
(let ((test-id (format "%s" (car test))))
;; a test is a list of 4 elements and the first element is a list itself
- (assert
+ (cl-assert
(and
(eq (length test) 4)
(listp (car test)))
@@ -761,22 +762,22 @@ relative ages.")
(mapc
(lambda (variant)
;; a variant is a list of 4 elements
- (assert (eq (length variant) 4) nil (concat test-id " 2"))
+ (cl-assert (eq (length variant) 4) nil (concat test-id " 2"))
(let ((files (coq-par-test-flatten-files (car test)))
(quick-mode (car variant))
(compilation-result (nth 1 variant))
(delete-result (nth 2 variant))
(req-obj-result (nth 3 variant)))
;; the delete field, when set, must be a member of the files list
- (assert (or (not delete-result)
+ (cl-assert (or (not delete-result)
(member delete-result files))
nil (concat test-id " 3"))
;; 8.4 compatibility check
(when (and (or (eq quick-mode 'no-quick) (eq quick-mode 'ensure-vo))
(not (member 'vio files)))
- (assert (not delete-result)
+ (cl-assert (not delete-result)
nil (concat test-id " 4"))
- (assert (eq compilation-result
+ (cl-assert (eq compilation-result
(not (eq (car (last (car test))) 'vo)))
nil (concat test-id " 5")))))
(cdr test))))
@@ -789,7 +790,7 @@ relative ages.")
((eq sym 'dep) "dep.vo")
((eq sym 'vo) "a.vo")
((eq sym 'vio) "a.vio")
- (t (assert nil)))))
+ (t (cl-assert nil)))))
(concat dir "/" file)))
(defun test-coq-par-one-test (counter dir file-descr variant dep-just-compiled)
@@ -832,7 +833,7 @@ test the result and side effects wth `assert'."
;; different-counter (current-time))
(setq different-not-ok nil)
(setq different-counter (1- different-counter))
- (assert (> different-counter 0)
+ (cl-assert (> different-counter 0)
nil "create files with different time stamps failed")
(dolist (same-descr file-descr)
(when (symbolp same-descr)
@@ -845,7 +846,7 @@ test the result and side effects wth `assert'."
(setq same-not-ok t)
(while same-not-ok
(setq same-counter (1- same-counter))
- (assert (> same-counter 0)
+ (cl-assert (> same-counter 0)
nil "create files with same time stamp filed")
(dolist (file file-list)
(with-temp-file file t))
@@ -875,40 +876,40 @@ test the result and side effects wth `assert'."
(put job 'youngest-coqc-dependency 'just-compiled))
(setq result (coq-par-job-needs-compilation job))
;; check result
- (assert (eq result compilation-result)
+ (cl-assert (eq result compilation-result)
nil (concat id " result"))
;; check file deletion
- (assert (or (not delete-result)
+ (cl-assert (or (not delete-result)
(not (file-attributes
(test-coq-par-sym-to-file dir delete-result))))
nil (concat id " delete file"))
;; check no other file is deleted
(dolist (f file-descr-flattened)
(unless (eq f delete-result)
- (assert (file-attributes (test-coq-par-sym-to-file dir f))
+ (cl-assert (file-attributes (test-coq-par-sym-to-file dir f))
nil (format "%s non del file %s: %s"
id f
(test-coq-par-sym-to-file dir f)))))
;; check value of 'required-obj-file property
- (assert (equal (get job 'required-obj-file)
+ (cl-assert (equal (get job 'required-obj-file)
(test-coq-par-sym-to-file dir req-obj-result))
nil (concat id " required-obj-file"))
;; check 'obj-mod-time property
(if obj-mod-result
- (assert
+ (cl-assert
(equal
(get job 'obj-mod-time)
(nth 5 (file-attributes
(test-coq-par-sym-to-file dir obj-mod-result))))
nil (concat id " obj-mod-time non nil"))
- (assert (not (get job 'obj-mod-time))
+ (cl-assert (not (get job 'obj-mod-time))
nil (concat id " obj-mod-time nil")))
;; check 'use-quick property
- (assert (eq (not (not (and compilation-result (eq req-obj-result 'vio))))
+ (cl-assert (eq (not (not (and compilation-result (eq req-obj-result 'vio))))
(get job 'use-quick))
nil (concat id " use-quick"))
;; check vio2vo-needed property
- (assert (eq
+ (cl-assert (eq
(and (eq quick-mode 'quick-and-vio2vo)
(eq req-obj-result 'vio)
(or (eq delete-result 'vo)
diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el
index 4889ccaf..3cdcd02a 100644
--- a/coq/coq-seq-compile.el
+++ b/coq/coq-seq-compile.el
@@ -24,6 +24,7 @@
;;; Code:
+(eval-when-compile (require 'cl-lib))
(defvar queueitems) ; dynamic scope in p-s-extend-queue-hook
(require 'coq-compile-common)
@@ -335,8 +336,8 @@ function returns () if MODULE-ID comes from the standard library."
;; error-message)))
;; (coq-display-compile-response-buffer)
(error error-message)))
- (assert (<= (length result) 1)
- "Internal error in coq-seq-map-module-id-to-obj-file")
+ (cl-assert (<= (length result) 1)
+ "Internal error in coq-seq-map-module-id-to-obj-file")
(car-safe result)))
(defun coq-seq-check-module (coq-object-local-hash-symbol span module-id &optional from)
diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 15697354..72639bc6 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -1,9 +1,9 @@
-;;; coq-smie.el --- SMIE lexer, grammar, and indent rules for Coq
+;;; coq-smie.el --- SMIE lexer, grammar, and indent rules for Coq -*- 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
@@ -41,7 +41,7 @@
;;; Code:
(require 'coq-indent)
-(require 'smie nil 'noerror)
+(require 'smie)
; debugging
;(defmacro measure-time (&rest body)
@@ -64,21 +64,22 @@ indentation work well."
:group 'coq)
-(defun coq-string-suffix-p (str1 str2 &optional ignore-case)
+(defalias 'coq--string-suffix-p
+ ;; Replacement for emacs < 24.4, borrowed from sindikat at
+ ;; stackoverflow efficient if bytecompiled, builtin version is
+ ;; probably better when it exists
+ (if (fboundp 'string-suffix-p)
+ 'string-suffix-p
+ (lambda (str1 str2 &optional ignore-case)
"Return non-nil if STR1 is a prefix of STR2.
If IGNORE-CASE is non-nil, the comparison is done without paying
attention to case differences."
(let ((begin2 (- (length str2) (length str1)))
(end2 (length str2)))
(when (< begin2 0) (setq begin2 0)) ; to avoid negative begin2
- (eq t (compare-strings str1 nil nil str2 begin2 end2 ignore-case))))
+ (eq t (compare-strings str1 nil nil str2 begin2 end2 ignore-case))))))
+
-;; Replacement for emacs < 24.4, borrowed from sindikat at
-;; stackoverflow efficient if bytecompiled, builtin version is
-;; probably better when it exists
-(unless (fboundp 'string-suffix-p)
- (fset 'string-suffix-p 'coq-string-suffix-p)
- (declare-function string-suffix-p "smie"))
;; As any user defined notation ending with "." will break
;; proofgeneral synchronization anyway, let us consider that any
@@ -145,12 +146,13 @@ intros. or Proof foo.
the token of \".\" is simply \".\"."
(save-excursion
- (let ((p (point)) (beg (coq-find-real-start))) ; moves to real start of command
+ (let ((p (point)))
+ (coq-find-real-start) ; Move to real start of command.
(cond
((looking-at "BeginSubproof\\>") ". proofstart")
((looking-at "Proof\\>")
(forward-char 5)
- (coq-find-not-in-comment-forward "[^[:space:]]") ;; skip spaces and comments
+ (forward-comment (point-max))
(if (looking-at "\\.\\|with\\|using") ". proofstart" "."))
((or (looking-at "Next\\s-+Obligation\\>")
(coq-smie-detect-goal-command))
@@ -211,26 +213,28 @@ the token of \".\" is simply \".\"."
(defun coq-backward-token-fast-nogluing-dot-friends ()
(forward-comment (- (point)))
- (let ((pt (point)))
- (let* ((tok-punc (skip-syntax-backward "."))
- (str-punc (buffer-substring-no-properties pt (point)))
- (tok-other (if (zerop tok-punc) (skip-syntax-backward "w_'"))))
- ;; special case: if the symbols found end by "." or ";", then consider this last letter alone as a token
- (when (and (not (zerop tok-punc)) (string-match "\\s.+[.;]" str-punc))
- (skip-syntax-forward ".")
- (forward-char -1))
- (buffer-substring-no-properties pt (point)))))
+ (let* ((pt (point))
+ (tok-punc (skip-syntax-backward "."))
+ (str-punc (buffer-substring-no-properties pt (point))))
+ (if (zerop tok-punc) (skip-syntax-backward "w_'"))
+ ;; Special case: if the symbols found end by "." or ";",
+ ;; then consider this last letter alone as a token
+ (when (and (not (zerop tok-punc)) (string-match "\\s.+[.;]" str-punc))
+ (skip-syntax-forward ".")
+ (forward-char -1))
+ (buffer-substring-no-properties pt (point))))
(defun coq-forward-token-fast-nogluing-dot-friends ()
(forward-comment (point-max))
- (let ((pt (point)))
- (let* ((tok-punc (skip-syntax-forward "."))
- (str-punc (buffer-substring-no-properties pt (point)))
- (tok-other (if (zerop tok-punc) (skip-syntax-forward "w_'"))))
- ;; special case: if the symbols found end by "." or ";", then consider this last letter alone as a token
- (when (and (not (zerop tok-punc)) (string-match "\\s.+[.;]" str-punc))
- (forward-char -1))
- (buffer-substring-no-properties pt (point)))))
+ (let* ((pt (point))
+ (tok-punc (skip-syntax-forward "."))
+ (str-punc (buffer-substring-no-properties pt (point))))
+ (if (zerop tok-punc) (skip-syntax-forward "w_'"))
+ ;; Special case: if the symbols found end by "." or ";",
+ ;; then consider this last letter alone as a token
+ (when (and (not (zerop tok-punc)) (string-match "\\s.+[.;]" str-punc))
+ (forward-char -1))
+ (buffer-substring-no-properties pt (point))))
;; ignore-between is a description of pseudo delimiters of blocks that
;; should be jumped when searching. There is a bad interaction when
@@ -298,8 +302,7 @@ inside parenthesis)."
; if we find something to ignore, we directly jump to the
; corresponding openner
(if parop
- (let ((p (point))
- (parops ; corresponding matcher may be a list
+ (let ((parops ; corresponding matcher may be a list
(if (listp (car parop)) (car parop) (cons (car parop) nil))))
; go to corresponding closer or meet "."
;(message "newpatterns = %S" (append parops (cons "." nil)))
@@ -386,9 +389,9 @@ The point should be at the beginning of the command name."
(equal (point)
(save-excursion (coq-find-real-start))))
-(defun coq-is-bullet-token (tok) (string-suffix-p "bullet" tok))
-(defun coq-is-subproof-token (tok) (string-suffix-p "subproof" tok))
-(defun coq-is-dot-token (tok) (or (string-suffix-p "proofstart" tok)
+(defun coq-is-bullet-token (tok) (coq--string-suffix-p "bullet" tok))
+(defun coq-is-subproof-token (tok) (coq--string-suffix-p "subproof" tok))
+(defun coq-is-dot-token (tok) (or (coq--string-suffix-p "proofstart" tok)
(string-equal "." tok)))
(defun coq-is-cmdend-token (tok)
(or (coq-is-bullet-token tok) (coq-is-subproof-token tok) (coq-is-dot-token tok)))
@@ -509,7 +512,7 @@ The point should be at the beginning of the command name."
((member corresp '("Inductive" "CoInductive" "Variant")) ":= inductive")
((equal corresp "let") ":= let")
((equal corresp "where") ":= inductive") ;; inductive or fixpoint, nevermind
- ((or (looking-back "{" nil)) ":= record")
+ ((or (eq ?\{ (char-before))) ":= record")
(t ":=")))) ; a parenthesis stopped the search
@@ -541,8 +544,8 @@ The point should be at the beginning of the command name."
(cond
((member backtok '("." "Ltac")) "; tactic")
((equal backtok nil)
- (if (or (looking-back "(" nil) (looking-back "\\[")
- (and (looking-back "{" nil)
+ (if (or (memq (char-before) '(?\( ?\[))
+ (and (eq (char-before) ?\{)
(equal (coq-smie-backward-token) "{ subproof"))) ;; recursive call
"; tactic"
"; record"))))))
@@ -558,10 +561,10 @@ The point should be at the beginning of the command name."
(equal (coq-smie-backward-token) "; tactic")) ;; recursive
"|| tactic")
;; this is wrong half of the time but should not harm indentation
- ((and (equal backtok nil) (looking-back "(" nil)) "||")
+ ((and (equal backtok nil) (eq (char-before) '?\()) "||")
((equal backtok nil)
- (if (or (looking-back "\\[" nil)
- (and (looking-back "{" nil)
+ (if (or (eq (char-before) '?\[)
+ (and (eq (char-before) '?\{)
(equal (coq-smie-backward-token) "{ subproof"))) ;; recursive call
"|| tactic"
"||"))))))
@@ -618,7 +621,8 @@ The point should be at the beginning of the command name."
;; (forward-char -1)
;; (if (looking-at "{") "{ subproof" "} subproof"))
- ((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac\\|uconstr\\)" nil))
+ ((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac\\|uconstr\\)"
+ (- (point) 7)))
": ltacconstr")
((member tok '(":=" "::="))
@@ -848,113 +852,112 @@ Typical values are 2 or 4."
;; greatly simplify this file. We should ask Stefan Monnier how to
;; have two grammars with smie.
(defconst coq-smie-grammar
- (when (fboundp 'smie-prec2->grammar)
- (smie-prec2->grammar
- (smie-bnf->prec2
- '((exp
- (exp ":= def" exp)
- (exp ":=" exp) (exp ":= inductive" exp)
- (exp "||" exp) (exp "|" exp) (exp "=>" exp)
- (exp "xxx provedby" exp) (exp "as morphism" exp)
- (exp "with signature" exp)
- ("match" matchexp "with match" exp "end");expssss
- ("let" assigns "in let" exp) ;("eval in" assigns "in eval" exp) disabled
- ("fun" exp "=> fun" exp) ("if" exp "then" exp "else" exp)
- ("quantif exists" exp ", quantif" exp)
- ("forall" exp ", quantif" exp)
- ;;;
- ("(" exp ")") ("{|" exps "|}") ("{" exps "}")
- (exp "; tactic" exp) (exp "in tactic" exp) (exp "as" exp)
- (exp "by" exp) (exp "with" exp) (exp "|-" exp)
- (exp ":" exp) (exp ":<" exp) (exp "," exp)
- (exp "->" exp) (exp "<->" exp) (exp "&" exp)
- (exp "/\\" exp) (exp "\\/" exp)
- (exp "==" exp) (exp "=" exp) (exp "<>" exp) (exp "<=" exp)
- (exp "<" exp) (exp ">=" exp) (exp ">" exp)
- (exp "=?" exp) (exp "<=?" exp) (exp "<?" exp)
- (exp "^" exp)
- (exp "+" exp) (exp "-" exp)
- (exp "*" exp)
- (exp ": ltacconstr" exp)(exp ". selector" exp))
- ;; Having "return" here rather than as a separate rule in `exp' causes
- ;; it to be indented at a different level than "with".
- (matchexp (exp) (exp "as match" exp) (exp "in match" exp)
- (exp "return" exp) )
- (exps (affectrec) (exps "; record" exps))
- (affectrec (exp ":= record" exp))
- (assigns (exp ":= let" exp)) ;(assigns "; record" assigns)
-
- (moduledef (moduledecl ":= module" exp))
- (moduledecl (exp) (exp ":" moduleconstraint)
- (exp "<:" moduleconstraint))
- (moduleconstraint
- (exp) (exp ":= with" exp)
- (moduleconstraint "with module" "module" moduleconstraint))
-
- ;; To deal with indentation inside module declaration and inside
- ;; proofs, we rely on the lexer. The lexer detects "." terminator of
- ;; goal starter and returns the ". proofstart" and ". moduelstart"
- ;; tokens.
- (bloc ("{ subproof" commands "} subproof")
- (". proofstart" commands "Proof End")
- (". modulestart" commands "end module" exp)
- (moduledecl) (moduledef)
- (exp))
-
- (commands (commands "." commands)
- (commands "- bullet" commands)
- (commands "+ bullet" commands)
- (commands "* bullet" commands)
- (commands "-- bullet" commands)
- (commands "++ bullet" commands)
- (commands "** bullet" commands)
- (commands "--- bullet" commands)
- (commands "+++ bullet" commands)
- (commands "*** bullet" commands)
- (commands "---- bullet" commands)
- (commands "++++ bullet" commands)
- (commands "**** bullet" commands)
- ;; "with" of mutual definition should act like "."
- ;; same for "where" (introduction of a notation
- ;; after a inductive or fixpoint)
- (commands "with inductive" commands)
- (commands "with fixpoint" commands)
- (commands "where" commands)
- (bloc)))
-
-
- ;; Resolve the "trailing expression ambiguity" as in "else x -> b".
- ;; each line orders tokens by increasing priority
- ;; | C x => fun a => b | C2 x => ...
- ;;'((assoc "=>") (assoc "|") (assoc "|-" "=> fun")) ; (assoc ", quantif")
- '((assoc "- bullet") (assoc "+ bullet") (assoc "* bullet")
- (assoc "-- bullet") (assoc "++ bullet") (assoc "** bullet")
- (assoc "--- bullet") (assoc "+++ bullet") (assoc "*** bullet")
- (assoc "---- bullet") (assoc "++++ bullet") (assoc "**** bullet")
- (assoc ".")
- (assoc "with inductive" "with fixpoint" "where"))
- '((assoc ":= def" ":= inductive")
- (assoc "|") (assoc "=>")
- (assoc ":=") (assoc "xxx provedby")
- (assoc "as morphism") (assoc "with signature") (assoc "with match")
- (assoc "in let")
- (assoc "in eval") (assoc "=> fun") (assoc "then") (assoc ", quantif")
- (assoc "|| tactic") ;; FIXME: detecting "+ tactic" and "|| tactic" seems impossible
- (assoc "; tactic") (assoc "in tactic") (assoc "as" "by") (assoc "with")
- (assoc "|-") (assoc ":" ":<") (assoc ",")
- (assoc "else")
- (assoc "->") (assoc "<->")
- (assoc "&") (assoc "/\\") (assoc "\\/")
- (assoc "==") (assoc "=") (assoc "<" ">" "<=" ">=" "<>")
- (assoc "=?") (assoc "<=?") (assoc "<?") (assoc "^")
- (assoc "||") ;; FIXME: detecting "+ tactic" and "|| tactic" seems impossible
- (assoc "+") (assoc "-") (assoc "*")
- (assoc ": ltacconstr") (assoc ". selector"))
- '((assoc ":" ":<") (assoc "<"))
- '((assoc ". modulestart" "." ". proofstart") (assoc "Module def")
- (assoc "with module" "module") (assoc ":= module")
- (assoc ":= with") (assoc ":" ":<"))
- '((assoc ":= def") (assoc "; record") (assoc ":= record")))))
+ (smie-prec2->grammar
+ (smie-bnf->prec2
+ '((exp
+ (exp ":= def" exp)
+ (exp ":=" exp) (exp ":= inductive" exp)
+ (exp "||" exp) (exp "|" exp) (exp "=>" exp)
+ (exp "xxx provedby" exp) (exp "as morphism" exp)
+ (exp "with signature" exp)
+ ("match" matchexp "with match" exp "end") ;expssss
+ ("let" assigns "in let" exp) ;("eval in" assigns "in eval" exp) disabled
+ ("fun" exp "=> fun" exp) ("if" exp "then" exp "else" exp)
+ ("quantif exists" exp ", quantif" exp)
+ ("forall" exp ", quantif" exp)
+;;;
+ ("(" exp ")") ("{|" exps "|}") ("{" exps "}")
+ (exp "; tactic" exp) (exp "in tactic" exp) (exp "as" exp)
+ (exp "by" exp) (exp "with" exp) (exp "|-" exp)
+ (exp ":" exp) (exp ":<" exp) (exp "," exp)
+ (exp "->" exp) (exp "<->" exp) (exp "&" exp)
+ (exp "/\\" exp) (exp "\\/" exp)
+ (exp "==" exp) (exp "=" exp) (exp "<>" exp) (exp "<=" exp)
+ (exp "<" exp) (exp ">=" exp) (exp ">" exp)
+ (exp "=?" exp) (exp "<=?" exp) (exp "<?" exp)
+ (exp "^" exp)
+ (exp "+" exp) (exp "-" exp)
+ (exp "*" exp)
+ (exp ": ltacconstr" exp)(exp ". selector" exp))
+ ;; Having "return" here rather than as a separate rule in `exp' causes
+ ;; it to be indented at a different level than "with".
+ (matchexp (exp) (exp "as match" exp) (exp "in match" exp)
+ (exp "return" exp) )
+ (exps (affectrec) (exps "; record" exps))
+ (affectrec (exp ":= record" exp))
+ (assigns (exp ":= let" exp)) ;(assigns "; record" assigns)
+
+ (moduledef (moduledecl ":= module" exp))
+ (moduledecl (exp) (exp ":" moduleconstraint)
+ (exp "<:" moduleconstraint))
+ (moduleconstraint
+ (exp) (exp ":= with" exp)
+ (moduleconstraint "with module" "module" moduleconstraint))
+
+ ;; To deal with indentation inside module declaration and inside
+ ;; proofs, we rely on the lexer. The lexer detects "." terminator of
+ ;; goal starter and returns the ". proofstart" and ". moduelstart"
+ ;; tokens.
+ (bloc ("{ subproof" commands "} subproof")
+ (". proofstart" commands "Proof End")
+ (". modulestart" commands "end module" exp)
+ (moduledecl) (moduledef)
+ (exp))
+
+ (commands (commands "." commands)
+ (commands "- bullet" commands)
+ (commands "+ bullet" commands)
+ (commands "* bullet" commands)
+ (commands "-- bullet" commands)
+ (commands "++ bullet" commands)
+ (commands "** bullet" commands)
+ (commands "--- bullet" commands)
+ (commands "+++ bullet" commands)
+ (commands "*** bullet" commands)
+ (commands "---- bullet" commands)
+ (commands "++++ bullet" commands)
+ (commands "**** bullet" commands)
+ ;; "with" of mutual definition should act like "."
+ ;; same for "where" (introduction of a notation
+ ;; after a inductive or fixpoint)
+ (commands "with inductive" commands)
+ (commands "with fixpoint" commands)
+ (commands "where" commands)
+ (bloc)))
+
+
+ ;; Resolve the "trailing expression ambiguity" as in "else x -> b".
+ ;; each line orders tokens by increasing priority
+ ;; | C x => fun a => b | C2 x => ...
+ ;;'((assoc "=>") (assoc "|") (assoc "|-" "=> fun")) ; (assoc ", quantif")
+ '((assoc "- bullet") (assoc "+ bullet") (assoc "* bullet")
+ (assoc "-- bullet") (assoc "++ bullet") (assoc "** bullet")
+ (assoc "--- bullet") (assoc "+++ bullet") (assoc "*** bullet")
+ (assoc "---- bullet") (assoc "++++ bullet") (assoc "**** bullet")
+ (assoc ".")
+ (assoc "with inductive" "with fixpoint" "where"))
+ '((assoc ":= def" ":= inductive")
+ (assoc "|") (assoc "=>")
+ (assoc ":=") (assoc "xxx provedby")
+ (assoc "as morphism") (assoc "with signature") (assoc "with match")
+ (assoc "in let")
+ (assoc "in eval") (assoc "=> fun") (assoc "then") (assoc ", quantif")
+ (assoc "|| tactic") ;; FIXME: detecting "+ tactic" and "|| tactic" seems impossible
+ (assoc "; tactic") (assoc "in tactic") (assoc "as" "by") (assoc "with")
+ (assoc "|-") (assoc ":" ":<") (assoc ",")
+ (assoc "else")
+ (assoc "->") (assoc "<->")
+ (assoc "&") (assoc "/\\") (assoc "\\/")
+ (assoc "==") (assoc "=") (assoc "<" ">" "<=" ">=" "<>")
+ (assoc "=?") (assoc "<=?") (assoc "<?") (assoc "^")
+ (assoc "||") ;; FIXME: detecting "+ tactic" and "|| tactic" seems impossible
+ (assoc "+") (assoc "-") (assoc "*")
+ (assoc ": ltacconstr") (assoc ". selector"))
+ '((assoc ":" ":<") (assoc "<"))
+ '((assoc ". modulestart" "." ". proofstart") (assoc "Module def")
+ (assoc "with module" "module") (assoc ":= module")
+ (assoc ":= with") (assoc ":" ":<"))
+ '((assoc ":= def") (assoc "; record") (assoc ":= record"))))
"Parsing table for Coq. See `smie-grammar'.")
;; FIXME:
; Record rec:Set := {
@@ -1010,11 +1013,11 @@ Typical values are 2 or 4."
(defun coq-smie-rules (kind token)
"Indentation rules for Coq. See `smie-rules-function'.
KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
- (case kind
- (:elem (case token
- (basic proof-indent)))
- (:close-all t)
- (:list-intro
+ (pcase kind
+ (`:elem (pcase token
+ (`basic proof-indent)))
+ (`:close-all t)
+ (`:list-intro
(or (member token '("fun" "forall" "quantif exists" "with"))
;; We include "." in list-intro for the ". { .. } \n { .. }" so the
;; second {..} is aligned with the first rather than being indented as
@@ -1026,7 +1029,7 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
; (forward-char 1) ; skip de "."
; (equal (coq-smie-forward-token) "{ subproof"))
))
- (:after
+ (`:after
(cond
;; Override the default indent step added because of their presence
;; in smie-closer-alist.
@@ -1064,7 +1067,9 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
(not (coq-smie-is-ltacdef))
(not (coq-smie-is-inside-parenthesized-tactic))
(or (not (smie-rule-parent-p "; tactic"))
- (and smie--parent
+ ;; FIXME: Don't depend on SMIE's internals!
+ (and (boundp 'smie--parent)
+ smie--parent
(coq-smie--same-line-as-parent
(nth 1 smie--parent) (point)))))
coq-indent-semicolon-tactical
@@ -1089,7 +1094,7 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
(save-excursion (forward-char -1) (coq-find-real-start)
`(column . ,(+ coq-indent-modulestart (current-column)))))))
- (:before
+ (`:before
(cond
; ((and (member token '("{ subproof"))
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index bb32fc52..7a11a43f 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1,9 +1,9 @@
-;;; coq-syntax.el --- Font lock expressions for Coq
+;;; coq-syntax.el --- Font lock expressions for Coq -*- 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
@@ -19,6 +19,7 @@
;;; Code:
+(eval-when-compile (require 'cl-lib))
(require 'proof-syntax)
(require 'proof-utils) ; proof-locate-executable
(require 'coq-db)
@@ -509,12 +510,12 @@ so for the following reasons:
)
;; modules and section are indented like goal starters
-;;; PC TODO: this category is used only for indentation, because
-;;; scripting uses information from coq to decide if a goal is
-;;; started. Since it is impossible for some commands to know
-;;; syntactically if they start something (ex: Instance), the
-;;; right thing to do would be to indent only on "Proof." and forget
-;;; about this category for indentation.
+;; PC TODO: this category is used only for indentation, because
+;; scripting uses information from coq to decide if a goal is
+;; started. Since it is impossible for some commands to know
+;; syntactically if they start something (ex: Instance), the
+;; right thing to do would be to indent only on "Proof." and forget
+;; about this category for indentation.
(defvar coq-goal-starters-db
'(
@@ -986,14 +987,15 @@ so for the following reasons:
;; elle declare un module.
;; (la fonction vernac_declare_module dans toplevel/vernacentries)
-(defun coq-count-match (regexp strg)
- "Count the number of max. non-overlapping substring of STRG matching REGEXP.
+(defun coq-count-match (regexp str)
+ "Count the number of max. non-overlapping substring of STR matching REGEXP.
Empty matches are counted once."
- (let ((nbmatch 0) (str strg))
- (while (and (proof-string-match regexp str) (not (string-equal str "")))
- (incf nbmatch)
- (if (= (match-end 0) 0) (setq str (substring str 1))
- (setq str (substring str (match-end 0)))))
+ (let ((nbmatch 0) (pos 0) (end (length str))
+ (case-fold-search nil))
+ (while (and (< pos end)
+ (string-match regexp str pos))
+ (cl-incf nbmatch)
+ (setq pos (max (match-end 0) (1+ pos))))
nbmatch))
;; Module and or section openings are detected syntactically. Module
@@ -1008,12 +1010,16 @@ Used by `coq-goal-command-p'"
(let* ((match (coq-count-match "\\_<match\\_>" str))
(with (coq-count-match "\\_<with\\_>" str))
(letwith (+ (coq-count-match "\\_<let\\_>" str) (- with match)))
- (affect (coq-count-match ":=" str)))
- (and (proof-string-match "\\`\\(Module\\)\\_>" str)
+ (affect (coq-count-match ":=" str))
+ (case-fold-search nil))
+ (and (string-match "\\`\\(Module\\)\\_>" str)
(= letwith affect))))
(defun coq-section-command-p (str)
- (proof-string-match "\\`\\(Section\\|Chapter\\)\\_>" str))
+ (let ((case-fold-search nil))
+ (string-match "\\`\\(Section\\|Chapter\\)\\_>" str)))
+
+(defvar coq-goal-command-regexp)
;; unused anymore (for good)
(defun coq-goal-command-str-p (str)
@@ -1022,16 +1028,17 @@ Use ‘coq-goal-command-p’ on a span instead if possible."
(let* ((match (coq-count-match "\\_<match\\_>" str))
(with (- (coq-count-match "\\_<with\\_>" str) (coq-count-match "\\_<with\\s-+signature\\_>" str)))
(letwith (+ (coq-count-match "\\_<let\\_>" str) (- with match)))
- (affect (coq-count-match ":=" str)))
- (and (proof-string-match coq-goal-command-regexp str)
+ (affect (coq-count-match ":=" str))
+ (case-fold-search nil))
+ (and (string-match coq-goal-command-regexp str)
(not
(and
- (proof-string-match
+ (string-match
(concat "\\`\\(Local\\|Definition\\|Lemma\\|Theorem\\|Fact\\|Add\\|Let\\|Program\\|Module\\|Class\\|Instance\\)\\_>")
str)
(not (= letwith affect))))
- (not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:"
- str)))))
+ (not (string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:"
+ str)))))
;; This is the function that tests if a SPAN is a goal start. All it
;; has to do is look at the 'goalcmd attribute of the span.
@@ -1062,8 +1069,15 @@ It is used:
(append coq-keywords-save-strict '("Proof"))
)
+;; According to Coq, "Definition" is both a declaration and a goal.
+;; It is understood here as being a goal. This is important for
+;; recognizing global identifiers, see coq-global-p.
+(defconst coq-save-command-regexp-strict
+ (proof-anchor-regexp
+ (concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save-strict)
+ "\\)")))
-(defun coq-save-command-p (span str)
+(defun coq-save-command-p (_span str)
"Decide whether argument is a Save command or not."
(or (proof-string-match coq-save-command-regexp-strict str)
(and (proof-string-match "\\`Proof\\_>" str)
@@ -1150,8 +1164,10 @@ It is used:
;; 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\\|"
+ (regexp-opt coq-reserved) "\\)"
+ "\\_>"))
(defvar coq-state-changing-tactics
(coq-build-regexp-list-from-db coq-tactics-db 'filter-state-changing))
@@ -1275,16 +1291,6 @@ It is used:
"*Font-lock table for Coq terms.")
-
-;; According to Coq, "Definition" is both a declaration and a goal.
-;; It is understood here as being a goal. This is important for
-;; recognizing global identifiers, see coq-global-p.
-(defconst coq-save-command-regexp-strict
- (proof-anchor-regexp
- (concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save-strict)
- "\\)")))
-
-
(defconst coq-save-command-regexp
(proof-anchor-regexp
(concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save)
@@ -1401,7 +1407,8 @@ part of another hypothesis.")
(search-forward-regexp coq-hyp-name-or-goalsep-in-goal-or-response-regexp nil t)
(goto-char (match-beginning 1))
;; if previous is a newline, don't include it i the overklay
- (when (looking-back "\\s-") (goto-char (- (point) 1)))
+ (when (looking-back "\\s-" (1- (point)))
+ (goto-char (- (point) 1)))
(point))))
; if several hyp names, we name the overlays with the first hyp name
(setq res
diff --git a/coq/coq.el b/coq/coq.el
index dfe519ef..06a01855 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -28,8 +28,6 @@
(require 'outline)
(require 'newcomment)
(require 'etags))
-(defvar smie-indent-basic)
-(defvar smie-rules-function)
(defvar proof-info) ; dynamic scope in proof-tree-urgent-action
(defvar action) ; dynamic scope in coq-insert-as stuff
(defvar string) ; dynamic scope in coq-insert-as stuff
@@ -51,17 +49,6 @@
(require 'coq-seq-compile) ; sequential compilation of Requires
(require 'coq-par-compile) ; parallel compilation of Requires
-;; for compilation in Emacs < 23.3 (NB: declare function only works at top level)
-(declare-function smie-bnf->prec2 "smie")
-(declare-function smie-rule-parent-p "smie")
-(declare-function smie-default-forward-token "smie")
-(declare-function smie-default-backward-token "smie")
-(declare-function smie-rule-prev-p "smie")
-(declare-function smie-rule-separator "smie")
-(declare-function smie-rule-parent "smie")
-
-(declare-function some "cl-extra") ; spurious bytecomp warning
-
;; prettify is in emacs > 24.4
;; FIXME: this should probably be done like for smie above.
(defvar coq-may-use-prettify (fboundp 'prettify-symbols-mode))
@@ -331,17 +318,7 @@ See also option `coq-hide-additional-subgoals'."
;; Indentation and navigation support via SMIE.
-(defcustom coq-use-smie t
- "OBSOLETE. smie code is always used now.
-
-If non-nil, Coq mode will try to use SMIE for indentation.
-SMIE is a navigation and indentation framework available in Emacs >= 23.3."
- :type 'boolean
- :group 'coq)
-
-(require 'smie nil 'noerror)
-(require 'coq-smie nil 'noerror)
-
+(require 'coq-smie)
;;
;; Auxiliary code for Coq modes
@@ -352,8 +329,8 @@ SMIE is a navigation and indentation framework available in Emacs >= 23.3."
"Return a list of frames displaying both response and goals buffers."
(let* ((wins-resp (get-buffer-window-list proof-response-buffer nil t))
(wins-gls (get-buffer-window-list proof-goals-buffer nil t))
- (frame-resp (cl-mapcar 'window-frame wins-resp))
- (frame-gls (cl-mapcar 'window-frame wins-gls)))
+ (frame-resp (mapcar #'window-frame wins-resp))
+ (frame-gls (mapcar #'window-frame wins-gls)))
(filtered-frame-list (lambda (x) (and (member x frame-resp) (member x frame-gls))))))
@@ -683,7 +660,7 @@ If locked span already has a state number, then do nothing. Also updates
;; This hook seems the one we want.
;; WARNING! It is applied once after each command PLUS once before a group of
;; commands is started
-(add-hook 'proof-state-change-hook 'coq-set-state-infos)
+(add-hook 'proof-state-change-hook #'coq-set-state-infos)
(defun count-not-intersection (l notin)
@@ -1028,7 +1005,7 @@ UNSETCMD. See `coq-command-with-set-unset'."
(concat " -\"" s "\""))
(defun coq-build-removed-patterns (l)
- (mapcar 'coq-build-removed-pattern l))
+ (mapcar #'coq-build-removed-pattern l))
(defsubst coq-put-into-quotes (s)
(concat "\"" s "\""))
@@ -1219,10 +1196,10 @@ Printing All set."
(setq symb val) ;; FIXME this is wrong (it should be 'set', but it would set nil sometimes)
(if coq-auto-adapt-printing-width
(progn
- (add-hook 'proof-assert-command-hook 'coq-adapt-printing-width)
- (add-hook 'proof-retract-command-hook 'coq-reset-printing-width))
- (remove-hook 'proof-assert-command-hook 'coq-adapt-printing-width)
- (remove-hook 'proof-retract-command-hook 'coq-reset-printing-width)))
+ (add-hook 'proof-assert-command-hook #'coq-adapt-printing-width)
+ (add-hook 'proof-retract-command-hook #'coq-reset-printing-width))
+ (remove-hook 'proof-assert-command-hook #'coq-adapt-printing-width)
+ (remove-hook 'proof-retract-command-hook #'coq-reset-printing-width)))
;; In case of nested proofs (which are announced as obsolete in future versions
;; of coq) Coq does not show the goals of enclosing proof when closing a nested
@@ -1258,13 +1235,13 @@ be called and no command will be sent to Coq."
;; silent (there is no goal to show).
(string-match "Backtrack" cmd))
(list "Unset Silent."))))
-
+
(defpacustom auto-adapt-printing-width t
"If non-nil, adapt automatically printing width of goals window.
Each timme the user sends abunch of commands to Coq, check if the
width of the goals window changed, and adapt coq printing width.
WARNING: If several windows are displaying the goals buffer, one
-is chosen randomly. WARNING 2: when backtracking the printing
+is chosen arbitrarily. WARNING 2: when backtracking the printing
width is synchronized by coq (?!)."
:type 'boolean
:safe 'booleanp
@@ -1278,7 +1255,7 @@ width is synchronized by coq (?!)."
;; this initiates auto adapt printing width at start, by reading the config
;; var. Let us put this at the end of hooks to have a chance to read local
;; variables first.
-(add-hook 'coq-mode-hook 'coq-auto-adapt-printing-width t)
+(add-hook 'coq-mode-hook #'coq-auto-adapt-printing-width t)
(defvar coq-shell-current-line-width nil
"Current line width of the Coq printing width.
@@ -1347,7 +1324,7 @@ redisplayed."
(proof-shell-invisible-command (format "Set Printing Width %S." (- wdth 1)) t)
(setq coq-shell-current-line-width wdth)
;; Show iff show non nil and some proof is under way
- (when (and show (not (null (caddr (coq-last-prompt-info-safe)))))
+ (when (and show (not (null (cl-caddr (coq-last-prompt-info-safe)))))
(proof-shell-invisible-command (format "Show.") t nil 'no-error-display)))))
(defun coq-adapt-printing-width-and-show(&optional show width)
@@ -1453,9 +1430,9 @@ Maintained by a hook in `proof-shell-handle-delayed-output-hook'.")
(positions (cdr hyp-positions))
(begcross (car positions))
(beghypname (cadr positions))
- (endhypname (caddr positions))
- (beg (cadddr positions))
- (end (cadddr (cdr positions))))
+ (endhypname (cl-caddr positions))
+ (beg (cl-cadddr positions))
+ (end (cl-cadddr (cdr positions))))
(let ((hypnameov (coq-make-hypname-overlay beghypname endhypname fstname buf))
(hypov (coq-make-hyp-overlay beg end fstname buf))
(crosshypov (coq-make-hypcross-overlay begcross (+ 1 begcross) fstname buf))
@@ -1568,10 +1545,10 @@ use `coq-unhighlight-hyp' to unhilight."
(coq-unhighlight-hyp-aux h)))
(defun coq-highlight-hyps (lh)
- (mapc 'coq-highlight-hyp lh))
+ (mapc #'coq-highlight-hyp lh))
(defun coq-unhighlight-hyps (lh)
- (mapc 'coq-unhighlight-hyp-aux lh))
+ (mapc #'coq-unhighlight-hyp-aux lh))
(defun coq-highlight-selected-hyps ()
"Highlight all hyps stored in `coq-highlighted-hyps'.
@@ -1606,7 +1583,7 @@ See `coq-highlight-hyps-cited-in-response' and `SearchAbout'."
Highlight always takes place in goals buffer."
(let ((inters (coq-get-hyps-cited-in-response)))
(coq-unhighlight-selected-hyps)
- (setq coq-highlighted-hyps (mapcar 'car inters))
+ (setq coq-highlighted-hyps (mapcar #'car inters))
(coq-highlight-selected-hyps)))
(defun coq-toggle-highlight-hyp (h)
@@ -1743,12 +1720,12 @@ See `coq-fold-hyp'."
(defun coq-unfold-hyp-list (lh)
"Fold the type of hypothesis in LH temporarily.
See `coq-unfold-hyp-aux'."
- (mapc 'coq-unfold-hyp-aux lh))
+ (mapc #'coq-unfold-hyp-aux lh))
(defun coq-fold-hyp-list (lh)
"Fold the type of hypothesis in LH temporarily.
See `coq-fold-hyp-aux'."
- (mapc 'coq-fold-hyp-aux lh))
+ (mapc #'coq-fold-hyp-aux lh))
(defun coq-fold-hyps ()
"Fold the type of hypothesis in LH durably.
@@ -1837,7 +1814,6 @@ See `coq-fold-hyp'."
;; *default* value to nil.
(custom-set-default 'proof-output-tooltips nil)
-;; This seems xemacs only code, remove?
(defconst coq-prettify-symbols-alist
'(("not" . ?¬)
;; ("/\\" . ?∧)
@@ -1966,7 +1942,7 @@ Near here means PT is either inside or just aside of a comment."
(setq proof-assistant-home-page coq-www-home-page)
(setq proof-prog-name coq-prog-name)
- (setq proof-guess-command-line 'coq-guess-command-line)
+ (setq proof-guess-command-line #'coq-guess-command-line)
(setq proof-prog-name-guess t)
;; We manage file saveing via coq-compile-auto-save and for coq
@@ -1991,26 +1967,25 @@ Near here means PT is either inside or just aside of a comment."
'(coq-compile-quick coq-compile-keep-going
coq-compile-auto-save coq-lock-ancestors))
- (setq proof-goal-command-p 'coq-goal-command-p
- proof-find-and-forget-fn 'coq-find-and-forget
- pg-topterm-goalhyplit-fn 'coq-goal-hyp
- proof-state-preserving-p 'coq-state-preserving-p)
+ (setq proof-goal-command-p #'coq-goal-command-p
+ proof-find-and-forget-fn #'coq-find-and-forget
+ pg-topterm-goalhyplit-fn #'coq-goal-hyp
+ proof-state-preserving-p #'coq-state-preserving-p)
(setq proof-query-identifier-command "Check %s.")
;;TODO: from v8.5 this wold be better:
;;(setq proof-query-identifier-command "About %s.")
(setq proof-save-command-regexp coq-save-command-regexp
- proof-really-save-command-p 'coq-save-command-p ;pierre:deals with Proof <term>.
+ proof-really-save-command-p #'coq-save-command-p ;pierre:deals with Proof <term>.
proof-save-with-hole-regexp coq-save-with-hole-regexp
proof-goal-with-hole-regexp coq-goal-with-hole-regexp
proof-nested-undo-regexp coq-state-changing-commands-regexp
proof-script-imenu-generic-expression coq-generic-expression)
- (when (fboundp 'smie-setup) ; always use smie, old indentation code removed
- (smie-setup coq-smie-grammar #'coq-smie-rules
- :forward-token #'coq-smie-forward-token
- :backward-token #'coq-smie-backward-token))
+ (smie-setup coq-smie-grammar #'coq-smie-rules
+ :forward-token #'coq-smie-forward-token
+ :backward-token #'coq-smie-backward-token)
;; old indentation code.
;; (require 'coq-indent)
@@ -2069,7 +2044,7 @@ Near here means PT is either inside or just aside of a comment."
(setq proof-cannot-reopen-processed-files nil)
- (add-hook 'proof-activate-scripting-hook 'proof-cd-sync nil t))
+ (add-hook 'proof-activate-scripting-hook #'proof-cd-sync nil t))
(defun coq-shell-mode-config ()
(setq
@@ -2199,13 +2174,13 @@ Near here means PT is either inside or just aside of a comment."
;
-;;; FIXME: to handle "printing all" properly, we should change the state
-;;; of the variables that also depend on it.
-;;; da:
+;; FIXME: to handle "printing all" properly, we should change the state
+;; of the variables that also depend on it.
+;; da:
-;;; pc: removed it and others of the same kind. Put an "option" menu instead,
-;;; with no state variable. To have the state we should use coq command that
-;;; output the value of the variables.
+;; pc: removed it and others of the same kind. Put an "option" menu instead,
+;; with no state variable. To have the state we should use coq command that
+;; output the value of the variables.
;(defpacustom print-fully-explicit nil
; "Print fully explicit terms."
; :type 'boolean
@@ -2335,7 +2310,7 @@ The not yet delayed output is in the region
proof-tree-show-subgoal))
proof-action-list))))))))))
-(add-hook 'proof-tree-urgent-action-hook 'coq-proof-tree-get-new-subgoals)
+(add-hook 'proof-tree-urgent-action-hook #'coq-proof-tree-get-new-subgoals)
(defun coq-find-begin-of-unfinished-proof ()
@@ -2464,7 +2439,7 @@ result of `coq-proof-tree-get-proof-info'."
;; finished the current proof
(coq-proof-tree-disable-evars)))))
-(add-hook 'proof-tree-urgent-action-hook 'coq-proof-tree-evar-display-toggle)
+(add-hook 'proof-tree-urgent-action-hook #'coq-proof-tree-evar-display-toggle)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -2488,7 +2463,7 @@ result of `coq-proof-tree-get-proof-info'."
(coq-bullet-p string)) ;; coq does not accept "Time -".
(setq string (concat coq--time-prefix string))))))
-(add-hook 'proof-shell-insert-hook 'coq-preprocessing)
+(add-hook 'proof-shell-insert-hook #'coq-preprocessing)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
@@ -2542,8 +2517,8 @@ mouse activation."
(string-match-p "\\.v\\'" s))
(defun coq-directories-files (l)
- (let* ((file-list-list (mapcar 'directory-files l))
- (file-list (apply 'append file-list-list))
+ (let* ((file-list-list (mapcar #'directory-files l))
+ (file-list (apply #'append file-list-list))
(filtered-list (cl-remove-if-not #'coq-postfix-.v-p file-list)))
filtered-list))
@@ -2558,7 +2533,7 @@ mouse activation."
(cleanpth (mapcar #'coq-load-path-to-paths pth))
(existingpth (cl-remove-if-not #'file-exists-p cleanpth))
(file-list (coq-directories-files existingpth)))
- (mapcar 'coq-remove-dot-v-extension file-list)))
+ (mapcar #'coq-remove-dot-v-extension file-list)))
(defun coq-insert-section-or-module ()
"Insert a module or a section after asking right questions."
@@ -2807,8 +2782,8 @@ Completion is on a quasi-exhaustive list of Coq tacticals."
;; Insertion commands
(define-key coq-keymap [(control ?i)] 'coq-insert-intros)
(define-key coq-keymap [(control ?m)] 'coq-insert-match)
-(define-key coq-keymap [(control ?()] 'coq-insert-section-or-module)
-(define-key coq-keymap [(control ?))] 'coq-end-Section)
+(define-key coq-keymap [(control ?\()] 'coq-insert-section-or-module)
+(define-key coq-keymap [(control ?\))] 'coq-end-Section)
(define-key coq-keymap [(control ?t)] 'coq-insert-tactic)
(define-key coq-keymap [?t] 'coq-insert-tactical)
(define-key coq-keymap [?!] 'coq-insert-solve-tactic) ; will work in tty
@@ -3014,7 +2989,7 @@ buffer."
(defun coq-highlight-error-hook ()
(coq-highlight-error t t))
-(add-hook 'proof-shell-handle-error-or-interrupt-hook 'coq-highlight-error-hook t)
+(add-hook 'proof-shell-handle-error-or-interrupt-hook #'coq-highlight-error-hook t)
;;
@@ -3111,9 +3086,9 @@ number of hypothesis displayed, without hiding the goal"
;; This hook must be added before coq-optimise-resp-windows, in order to be evaluated
;; *after* windows resizing.
(add-hook 'proof-shell-handle-delayed-output-hook
- 'coq-show-first-goal)
+ #'coq-show-first-goal)
(add-hook 'proof-shell-handle-delayed-output-hook
- 'coq-update-minor-mode-alist)
+ #'coq-update-minor-mode-alist)
(add-hook 'proof-shell-handle-delayed-output-hook
(lambda ()
(if (proof-string-match coq-shell-proof-completed-regexp
@@ -3133,7 +3108,7 @@ number of hypothesis displayed, without hiding the goal"
(<= (- (frame-height) (window-height)) 2))
;; bug fixed in generic ocde, useless now:
-;(add-hook 'proof-activate-scripting-hook '(lambda () (when proof-three-window-enable (proof-layout-windows))))
+;(add-hook 'proof-activate-scripting-hook (lambda () (when proof-three-window-enable (proof-layout-windows))))
;; *Experimental* auto shrink response buffer in three windows mode. Things get
;; a bit messed up if the response buffer is not at the right place (below
@@ -3183,9 +3158,11 @@ Only when three-buffer-mode is enabled."
;; i.e. added in hook AFTER it.
;; Adapt when displaying a normal message
-(add-hook 'proof-shell-handle-delayed-output-hook 'coq-optimise-resp-windows-if-option)
+(add-hook 'proof-shell-handle-delayed-output-hook
+ #'coq-optimise-resp-windows-if-option)
;; Adapt when displaying an error or interrupt
-(add-hook 'proof-shell-handle-error-or-interrupt-hook 'coq-optimise-resp-windows-if-option)
+(add-hook 'proof-shell-handle-error-or-interrupt-hook
+ #'coq-optimise-resp-windows-if-option)
;;; DOUBLE HIT ELECTRIC TERMINATOR
;; Trying to have double hit on colon behave like electric terminator. The "."
@@ -3315,7 +3292,7 @@ priority to the former."
;; when "compile when require" is off. When switching scripting buffer, let us
;; restart the coq shell process, so that it applies local coqtop options.
(add-hook 'proof-deactivate-scripting-hook
- 'coq-switch-buffer-kill-proof-shell ;; this function is in coq-compile-common
+ #'coq-switch-buffer-kill-proof-shell ;; this function is in coq-compile-common
t)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 14:44:16 +0000