diff options
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-mode.el | 261 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 28 | ||||
| -rw-r--r-- | coq/coq-system.el | 30 | ||||
| -rw-r--r-- | coq/coq.el | 277 |
4 files changed, 333 insertions, 263 deletions
diff --git a/coq/coq-mode.el b/coq/coq-mode.el new file mode 100644 index 00000000..f5d40027 --- /dev/null +++ b/coq/coq-mode.el @@ -0,0 +1,261 @@ +;;; coq-mode.el --- Major mode for Coq proof assistant -*- 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, 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 +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + +;; Authors: Healfdene Goguen, Pierre Courtieu +;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr> + +;; License: GPL (GNU GENERAL PUBLIC LICENSE) + +;;; Commentary: +;; + +;;; Code: + +(unless (locate-library "coq-mode") + (add-to-list 'load-path + (expand-file-name + (file-name-directory (or load-file-name buffer-file-name))))) + +;; (if t (require 'coq nil 'noerror)) +(require 'coq-smie) +(require 'coq-syntax) ;For font-lock-keywords + +(defgroup coq-mode () + "Major mode to edit Coq code." + :group 'programming) + +;; 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)) + +(defcustom coq-prog-name + (or (if (executable-find "coqtop") "coqtop") + (let ((exec-path (append exec-path '("C:/Program Files/Coq/bin")))) + (executable-find "coqtop")) + "coqtop") + "Name of program to run as Coq. +On Windows with latest Coq package you might need something like: + C:/Program Files/Coq/bin/coqtop.opt.exe +instead of just \"coqtop\". +This must be a single program name with no arguments. See option +`coq-prog-args' to manually adjust the arguments to the Coq process. +See also `coq-prog-env' to adjust the environment." + :type 'string + :group 'coq + :group 'coq-mode) + +(defun get-coq-library-directory () + (let ((default-directory + (if (file-accessible-directory-p default-directory) + default-directory + "/"))) + (or (ignore-errors (car (process-lines coq-prog-name "-where"))) + "/usr/local/lib/coq"))) + +(defconst coq-library-directory (get-coq-library-directory) ;; FIXME Should be refreshed more often + "The coq library directory, as reported by \"coqtop -where\".") + +(defcustom coq-tags (expand-file-name "/theories/TAGS" coq-library-directory) + "The default TAGS table for the Coq library." + :type 'string) + +(defcustom coq-use-pg t + "If non-nil, activate the ProofGeneral backend." + :type 'boolean) + +;; prettify is in emacs > 24.4 +(defvar prettify-symbols-alist) + +(defconst coq-prettify-symbols-alist + '(("not" . ?¬) + ;; ("/\\" . ?∧) + ("/\\" . ?⋀) + ;; ("\\/" . ?∨) + ("\\/" . ?⋁) + ;;("forall" . ?∀) + ("forall" . ?Π) + ("fun" . ?λ) + ("->" . ?→) + ("<-" . ?←) + ("=>" . ?⇒) + ;; ("~>" . ?↝) ;; less desirable + ;; ("-<" . ?↢) ;; Paterson's arrow syntax + ;; ("-<" . ?⤙) ;; nicer but uncommon + ("::" . ?∷) + )) + +(defvar coq-mode-map + (let ((map (make-sparse-keymap))) + map) + "Keymap for `coq-mode'.") + +(defvar coq-mode-syntax-table + (let ((st (make-syntax-table))) + (modify-syntax-entry ?\$ "." st) + (modify-syntax-entry ?\/ "." st) + (modify-syntax-entry ?\\ "." st) + (modify-syntax-entry ?+ "." st) + (modify-syntax-entry ?- "." st) + (modify-syntax-entry ?= "." st) + (modify-syntax-entry ?% "." st) + (modify-syntax-entry ?< "." st) + (modify-syntax-entry ?> "." st) + (modify-syntax-entry ?\& "." st) + (modify-syntax-entry ?_ "_" st) ; beware: word consituent EXCEPT in head position + (modify-syntax-entry ?\' "_" st) ; always word constituent + (modify-syntax-entry ?∀ "." st) + (modify-syntax-entry ?∃ "." st) + (modify-syntax-entry ?λ "." st) ;; maybe a bad idea... lambda is a letter + (modify-syntax-entry ?\| "." st) + + ;; Should maybe be "_" but it makes coq-find-and-forget (in coq.el) bug, + ;; hence the coq-with-altered-syntax-table to put "." into "_" class + ;; temporarily. + (modify-syntax-entry ?\. "." st) + + (modify-syntax-entry ?\* ". 23n" st) + (modify-syntax-entry ?\( "()1" st) + (modify-syntax-entry ?\) ")(4" st) + st)) + +;; FIXME, deal with interactive "Definition" +(defvar coq-outline-regexp + ;; (concat "(\\*\\|" + (concat "[ ]*" (regexp-opt + '( + "Ltac" "Corr" "Modu" "Sect" "Chap" "Goal" + "Definition" "Lemm" "Theo" "Fact" "Rema" + "Mutu" "Fixp" "Func") + t))) + +(defvar coq-outline-heading-end-regexp "\\.[ \t\n]") + +(defun coq-near-comment-region () + "Return a list of the forme (BEG END). +BEG,END being is the comment region near position PT. +Return nil if PT is not near a comment. +Near here means PT is either inside or just aside of a comment." + (save-excursion + (let ((pos (point)) + (ppss (syntax-ppss (1- (point))))) + (unless (nth 4 ppss) + ;; We're not squarely inside a comment, nor at its end. + ;; But we may still be at the beginning of a comment. + (setq ppss (syntax-ppss + (+ pos (if (looking-at comment-start-skip) 2 1))))) + (when (nth 4 ppss) + (goto-char (nth 8 ppss)) + (list (point) + (progn (forward-comment 1) (point))))))) + + +(defun coq-fill-paragraph-function (_n) + "Coq mode specific fill-paragraph function. Fills only comment at point." + (let ((reg (coq-near-comment-region))) + (when reg + (fill-region (car reg) (cadr reg)))) + t);; true to not fallback to standard fill function + +;; TODO (but only for paragraphs in comments) +;; Should recognize coqdoc bullets, stars etc... Unplugged for now. +(defun coq-adaptive-fill-function () + (let ((reg (coq-near-comment-region))) + (save-excursion + (goto-char (car reg)) + (re-search-forward "\\((\\*+ ?\\)\\( *\\)") + (let* ((cm-start (match-string 1)) + (cm-prefix (match-string 2))) + (concat (make-string (length cm-start) ? ) cm-prefix))))) + +;;;###autoload +(add-to-list 'auto-mode-alist '("\\.v\\'" . coq-mode)) + +(defun coq--parent-mode () + (if coq-use-pg (proof-mode) (prog-mode))) + +;;;###autoload +(define-derived-mode coq-mode coq--parent-mode "Coq" + "Major mode for Coq scripts. + +\\{coq-mode-map}" + ;; SMIE needs this. + (set (make-local-variable 'parse-sexp-ignore-comments) t) + ;; Coq error messages are thrown off by TAB chars. + (set (make-local-variable 'indent-tabs-mode) nil) + ;; Coq defninition never start by a parenthesis + (set (make-local-variable 'open-paren-in-column-0-is-defun-start) nil) + ;; do not break lines in code when filling + (set (make-local-variable 'fill-nobreak-predicate) + (lambda () (not (nth 4 (syntax-ppss))))) + ;; coq mode specific indentation function + (set (make-local-variable 'fill-paragraph-function) + #'coq-fill-paragraph-function) + + ;; TODO (but only for paragraphs in comments) + ;; (set (make-local-variable 'paragraph-start) "[ ]*\\((\\**\\|$\\)") + ;; (set (make-local-variable 'paragraph-separate) "\\**) *$\\|$") + ;; (set (make-local-variable 'adaptive-fill-function) + ;; #'coq-adaptive-fill-function) + + (set (make-local-variable 'comment-start-skip) "(\\*+ *") + (set (make-local-variable 'comment-end-skip) " *\\*+)") + + (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) + ;; (setq + ;; ;; indentation is implemented in coq-indent.el + ;; indent-line-function #'coq-indent-line + ;; proof-indent-any-regexp coq-indent-any-regexp + ;; proof-indent-open-regexp coq-indent-open-regexp + ;; proof-indent-close-regexp coq-indent-close-regexp) + ;; (set (make-local-variable 'indent-region-function) #'coq-indent-region) + + ;; we can cope with nested comments + (set (make-local-variable 'comment-quote-nested) nil) + + ;; FIXME: have abbreviation without holes + ;(if coq-use-editing-holes (holes-mode 1)) + (if (fboundp 'holes-mode) (holes-mode 1)) + + ;; Setup Proof-General interface to Coq. + (if coq-use-pg (coq-pg-setup)) + + ;; font-lock + (setq-local font-lock-defaults '(coq-font-lock-keywords-1)) + + ;; outline + (setq-local outline-regexp coq-outline-regexp) + (setq-local outline-heading-end-regexp coq-outline-heading-end-regexp) + + ;; tags + (if (file-exists-p coq-tags) + (set (make-local-variable 'tags-table-list) + (cons coq-tags tags-table-list))) + + (set (make-local-variable 'blink-matching-paren-dont-ignore-comments) t) + + (when coq-may-use-prettify + (set (make-local-variable 'prettify-symbols-alist) + coq-prettify-symbols-alist))) + +(provide 'coq-mode) + +;; Local Variables: *** +;; fill-column: 79 *** +;; indent-tabs-mode: nil *** +;; coding: utf-8 *** +;; End: *** + +;;; coq-mode.el ends here diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 7a11a43f..30f1a374 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1454,34 +1454,6 @@ part of another hypothesis.") -(defun coq-init-syntax-table () - "Set appropriate values for syntax table in current buffer." - - (modify-syntax-entry ?\$ ".") - (modify-syntax-entry ?\/ ".") - (modify-syntax-entry ?\\ ".") - (modify-syntax-entry ?+ ".") - (modify-syntax-entry ?- ".") - (modify-syntax-entry ?= ".") - (modify-syntax-entry ?% ".") - (modify-syntax-entry ?< ".") - (modify-syntax-entry ?> ".") - (modify-syntax-entry ?\& ".") - (modify-syntax-entry ?_ "_") ; beware: word consituent EXCEPT in head position - (modify-syntax-entry ?\' "_") ; always word constituent - (modify-syntax-entry ?∀ ".") - (modify-syntax-entry ?∃ ".") - (modify-syntax-entry ?λ ".") ;; maybe a bad idea... lambda is a letter - (modify-syntax-entry ?\| ".") - - ;; should maybe be "_" but it makes coq-find-and-forget (in coq.el) bug - ;; Hence the coq-with-altered-syntax-table below to put "." into "_" class temporarily - (modify-syntax-entry ?\. ".") - - (modify-syntax-entry ?\* ". 23n") - (modify-syntax-entry ?\( "()1") - (modify-syntax-entry ?\) ")(4")) - ;; use this to evaluate code with "." being consisdered a symbol ;; constituent (better behavior for thing-at and maybe font-lock too, ;; for indentation we use ad hoc smie lexers). diff --git a/coq/coq-system.el b/coq/coq-system.el index e89a0fdb..44a774ae 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -24,6 +24,7 @@ ;;; Code: (require 'proof) +(require 'coq-mode) ;for coq-prog-name (defvar coq-prog-args) (defvar coq-debug) @@ -43,19 +44,6 @@ On Windows you might need something like: (setq coq-prog-env '(\"HOME=C:\\Program Files\\Coq\\\"))" :group 'coq) -(defcustom coq-prog-name - (if (executable-find "coqtop") "coqtop" - (proof-locate-executable "coqtop" t '("C:/Program Files/Coq/bin"))) - "*Name of program to run as Coq. See `proof-prog-name', set from this. -On Windows with latest Coq package you might need something like: - C:/Program Files/Coq/bin/coqtop.opt.exe -instead of just \"coqtop\". -This must be a single program name with no arguments. See option -`coq-prog-args' to manually adjust the arguments to the Coq process. -See also `coq-prog-env' to adjust the environment." - :type 'string - :group 'coq) - (defcustom coq-dependency-analyzer (if (executable-find "coqdep") "coqdep" (proof-locate-executable "coqdep" t '("C:/Program Files/Coq/bin"))) @@ -70,22 +58,6 @@ See also `coq-prog-env' to adjust the environment." :type 'string :group 'coq) -(defun get-coq-library-directory () - (let ((default-directory - (if (file-accessible-directory-p default-directory) - default-directory - "/"))) - (or (ignore-errors (car (process-lines coq-prog-name "-where"))) - "/usr/local/lib/coq"))) - -(defconst coq-library-directory (get-coq-library-directory) ;; FIXME Should be refreshed more often - "The coq library directory, as reported by \"coqtop -where\".") - -(defcustom coq-tags (concat coq-library-directory "/theories/TAGS") - "The default TAGS table for the Coq library." - :type 'string - :group 'coq) - (defcustom coq-pinned-version nil "Which version of Coq you are using. There should be no need to set this value unless you use the trunk from @@ -19,6 +19,16 @@ ;;; Code: +;; PG doesn't support using several backends at the same time. +;; FIXME: We really should set proof-assistant just because this file is +;; loaded (e.g. we should set it within coq-pg-setup instead), but +;; defpacustom and various others fail if executed before proof-assistant +;; is set. +(if (and (boundp 'proof-assistant) + (member proof-assistant '(nil "" "Coq" "coq"))) + (proof-ready-for-assistant 'coq) + (message "Coq-PG error: Proof General already in use for %s" proof-assistant)) + (require 'cl-lib) (require 'span) @@ -43,15 +53,11 @@ (require 'proof) (require 'coq-system) ; load path, option, project file etc. (require 'coq-syntax) ; font-lock, syntax categories (tactics, commands etc) -(require 'coq-local-vars) ; setting coq args via file variables +(require 'coq-local-vars) ; setting coq args via file variables ; (prefer _CoqProject file instead) (require 'coq-abbrev) ; abbrev and coq specific menu (require 'coq-seq-compile) ; sequential compilation of Requires (require 'coq-par-compile) ; parallel compilation of Requires - -;; 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)) (defvar prettify-symbols-alist) @@ -81,7 +87,7 @@ These are appended at the end of `coq-shell-init-cmd'." :group 'coq) ;; Default coq is only Private_ and _subproof -(defcustom coq-search-blacklist-string ; add this? \"_ind\" \"_rect\" \"_rec\" +(defcustom coq-search-blacklist-string ; add this? \"_ind\" \"_rect\" \"_rec\" "\"Private_\" \"_subproof\"" "String for blacklisting strings from requests to Coq environment." :type 'string @@ -161,7 +167,7 @@ See also option `coq-hide-additional-subgoals'." ;; Ignore all commands that start a proof. Otherwise "Proof" will appear ;; as superfluous node in the proof tree. Note that we cannot ignore Proof, -;; because, Fixpoint does not display the proof goal, see Coq bug #2776. +;; because, Fixpoint does not display the proof goal, see Coq bug #2776. (defcustom coq-proof-tree-ignored-commands-regexp (concat "^\\(\\(Show\\)\\|\\(Locate\\)\\|" "\\(Theorem\\)\\|\\(Lemma\\)\\|\\(Remark\\)\\|\\(Fact\\)\\|" @@ -264,18 +270,6 @@ See also option `coq-hide-additional-subgoals'." ;; Outline mode ;; -;; FIXME, deal with interacive "Definition" -(defvar coq-outline-regexp -;; (concat "(\\*\\|" - (concat "[ ]*" (regexp-opt - '( - "Ltac" "Corr" "Modu" "Sect" "Chap" "Goal" - "Definition" "Lemm" "Theo" "Fact" "Rema" - "Mutu" "Fixp" "Func") t))) -;;) - -(defvar coq-outline-heading-end-regexp "\\.[ \t\n]") - (defvar coq-shell-outline-regexp coq-goal-regexp) (defvar coq-shell-outline-heading-end-regexp coq-goal-regexp) @@ -298,6 +292,10 @@ See also option `coq-hide-additional-subgoals'." ;; Derived modes ;; +(defvar coq-shell-mode-syntax-table coq-mode-syntax-table) +(defvar coq-response-mode-syntax-table coq-mode-syntax-table) +(defvar coq-goals-mode-syntax-table coq-mode-syntax-table) + (define-derived-mode coq-shell-mode proof-shell-mode "Coq Shell" nil (coq-shell-mode-config)) @@ -305,21 +303,10 @@ See also option `coq-hide-additional-subgoals'." (define-derived-mode coq-response-mode proof-response-mode "Coq Response" nil (coq-response-config)) - -(define-derived-mode coq-mode proof-mode "Coq" - "Major mode for Coq scripts. - -\\{coq-mode-map}" - (coq-mode-config)) - (define-derived-mode coq-goals-mode proof-goals-mode "Coq Goals" nil (coq-goals-mode-config)) -;; Indentation and navigation support via SMIE. - -(require 'coq-smie) - ;; ;; Auxiliary code for Coq modes ;; @@ -385,7 +372,7 @@ annotation-start) if found." ;; This is a modified version of the same function in generic/proof-shell.el. ;; Using function coq-search-urgent-message instead of regex ;; proof-shell-eager-annotation-start, in order to let non urgent message as -;; such. i.e. "Time" messages. +;; such. i.e. "Time" messages. (defun proof-shell-process-urgent-messages () "Scan the shell buffer for urgent messages. Scanning starts from `proof-shell-urgent-message-scanner' or @@ -424,7 +411,7 @@ This is a subroutine of `proof-shell-filter'." ;; Set position of last urgent message found (if lastend (set-marker proof-shell-urgent-message-marker lastend)) - + (goto-char pt))) ;; Due to the architecture of proofgeneral, informative message put *before* @@ -456,13 +443,13 @@ This is a subroutine of `proof-shell-filter'." (pg-response-display-with-face strnotrailingspace))) ; face -;;;;;;;;;;; Trying to accept { and } as terminator for empty commands. Actually -;;;;;;;;;;; I am experimenting two new commands "{" and "}" (without no -;;;;;;;;;;; trailing ".") which behave like BeginSubProof and EndSubproof. The -;;;;;;;;;;; absence of a trailing "." makes it difficult to distinguish between -;;;;;;;;;;; "{" of normal coq code (implicits, records) and this the new -;;;;;;;;;;; commands. We therefore define a coq-script-parse-function to this -;;;;;;;;;;; purpose. +;; Trying to accept { and } as terminator for empty commands. Actually +;; I am experimenting two new commands "{" and "}" (without no +;; trailing ".") which behave like BeginSubProof and EndSubproof. The +;; absence of a trailing "." makes it difficult to distinguish between +;; "{" of normal coq code (implicits, records) and this the new +;; commands. We therefore define a coq-script-parse-function to this +;; purpose. ;; coq-end-command-regexp is ni coq-indent.el (defconst coq-script-command-end-regexp coq-end-command-regexp) @@ -981,7 +968,7 @@ UNSETCMD. See `coq-command-with-set-unset'." ;; (let* ((cmd) (postform (if (eq postformatcmd nil) 'identity postformatcmd))) - + ;; (proof-shell-ready-prover) ;; (setq cmd (coq-guess-or-ask-for-string ask dontguess)) @@ -1218,7 +1205,7 @@ be called and no command will be sent to Coq." ;; If closing a nested proof, Show the enclosing goal. (and (string-match coq-save-command-regexp-strict cmd) (> (length coq-last-but-one-proofstack) 1)) - ;; If user issued a printing option then t printing. + ;; If user issued a printing option then t printing. (and (string-match "\\(S\\|Uns\\)et\\s-+Printing" cmd) (> (length coq-last-but-one-proofstack) 0))) (list "Show.")) @@ -1285,7 +1272,7 @@ necessary.") (coq-buffer-window-width proof-goals-buffer)) (defun coq-response-window-width () (coq-buffer-window-width proof-response-buffer)) - + (defun coq-guess-goal-buffer-at-next-command () "Return the probable width of goals buffer if it pops up now. This is a guess based on the current width of goals buffer if @@ -1400,7 +1387,7 @@ Maintained by a hook in `proof-shell-handle-delayed-output-hook'.") ;; coq-hyp...faces (defun coq-make-hypcross-overlay (beg end h buf) (let ((ov (make-overlay beg end buf))) - (when ov + (when ov (overlay-put ov 'evaporate t) (overlay-put ov 'is-hypcross t) (overlay-put ov 'hyp-name h) @@ -1441,7 +1428,7 @@ Maintained by a hook in `proof-shell-handle-delayed-output-hook'.") (mapc (lambda (s) (setq res - (cons + (cons (cons (substring-no-properties s) (cons hypov (cons hypnameov (cons crosshypov nil)) )) res))) @@ -1601,7 +1588,7 @@ See `coq-highlight-hyp'." (or (car (coq-overlays-at pt 'hyp-name)) ;; we may be between hypname and hyp, so skip backward to ;; something meaningful - (save-excursion + (save-excursion (goto-char pt) (search-backward-regexp "[^ :=]\\|\n") (car (coq-overlays-at (point) 'hyp-name))))) @@ -1663,7 +1650,7 @@ Used on hyptohesis overlays in goals buffer mainly." (prefx (make-string (min 8 lgthhyp) ?.)) (hypcross-ov (overlay-get hyp-overlay 'hypcross-ov))) (overlay-put - hyp-overlay 'display + hyp-overlay 'display prefx ;(propertize prefx 'keymap coq-hidden-hyp-map) ) (overlay-put hyp-overlay 'evaporate t) @@ -1814,70 +1801,6 @@ See `coq-fold-hyp'." ;; *default* value to nil. (custom-set-default 'proof-output-tooltips nil) -(defconst coq-prettify-symbols-alist - '(("not" . ?¬) - ;; ("/\\" . ?∧) - ("/\\" . ?⋀) - ;; ("\\/" . ?∨) - ("\\/" . ?⋁) - ;;("forall" . ?∀) - ("forall" . ?Π) - ("fun" . ?λ) - ("->" . ?→) - ("<-" . ?←) - ("=>" . ?⇒) - ;; ("~>" . ?↝) ;; less desirable - ;; ("-<" . ?↢) ;; Paterson's arrow syntax - ;; ("-<" . ?⤙) ;; nicer but uncommon - ("::" . ?∷) - )) - - -(defun coq-get-comment-region (pt) - "Return a list of the form (BEG END). -BEG,END being the comment region arount position PT. -Return nil if PT is not inside a comment." - (save-excursion - (goto-char pt) - `(,(save-excursion (coq-find-comment-start)) - ,(save-excursion (coq-find-comment-end))))) - -(defun coq-near-comment-region () - "Return a list of the forme (BEG END). -BEG,END being is the comment region near position PT. -Return nil if PT is not near a comment. -Near here means PT is either inside or just aside of a comment." - (save-excursion - (cond - ((coq-looking-at-comment) - (coq-get-comment-region (point))) - ((and (looking-back proof-script-comment-end nil) - (save-excursion (forward-char -1) (coq-looking-at-comment))) - (coq-get-comment-region (- (point) 1))) - ((and (looking-at proof-script-comment-start) - (save-excursion (forward-char) (coq-looking-at-comment))) - (coq-get-comment-region (+ (point) 1)))))) - -(defun coq-fill-paragraph-function (n) - "Coq mode specific fill-paragraph function. Fills only comment at point." - (let ((reg (coq-near-comment-region))) - (when reg - (fill-region (car reg) (cadr reg)))) - t);; true to not fallback to standard fill function - -;; TODO (but only for paragraphs in comments) -;; Should recognize coqdoc bullets, stars etc... Unplugged for now. -(defun coq-adaptive-fill-function () - (let ((reg (coq-near-comment-region))) - (save-excursion - (goto-char (car reg)) - (re-search-forward "\\((\\*+ ?\\)\\( *\\)") - (let* ((cm-start (match-string 1)) - (cm-prefix (match-string 2))) - (concat (make-string (length cm-start) ? ) cm-prefix))))) - - - ;;;;;;;;;;;;;;;;;;;;;;;attempt to deal with debug mode ;;;;;;;;;;;;;;;; ;; tries to extract the last debug goal and display it in goals buffer @@ -1908,25 +1831,26 @@ Near here means PT is either inside or just aside of a comment." ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun coq-mode-config () - ;; SMIE needs this. - (set (make-local-variable 'parse-sexp-ignore-comments) t) - ;; Coq error messages are thrown off by TAB chars. - (set (make-local-variable 'indent-tabs-mode) nil) - ;; Coq defninition never start by a parenthesis - (set (make-local-variable 'open-paren-in-column-0-is-defun-start) nil) - ;; do not break lines in code when filling - (set (make-local-variable 'fill-nobreak-predicate) - (lambda () (not (nth 4 (syntax-ppss))))) - ;; coq mode specific indentation function - (set (make-local-variable 'fill-paragraph-function) 'coq-fill-paragraph-function) - - ;; TODO (but only for paragraphs in comments) - ;; (set (make-local-variable 'paragraph-start) "[ ]*\\((\\**\\|$\\)") - ;; (set (make-local-variable 'paragraph-separate) "\\**) *$\\|$") - ;; (set (make-local-variable 'adaptive-fill-function) 'coq-adaptive-fill-function) - +(defvar coq-pg-mode-map + (let ((map (make-sparse-keymap))) + (set-keymap-parent map proof-mode-map) + + ;;(define-key coq-mode-map coq-double-hit-hot-key 'coq-terminator-insert) + + ;; Setting the new mapping for terminator, overrides the following in + ;; proof-script: + ;; (define-key proof-mode-map (vector (aref proof-terminal-string 0)) + ;; #'proof-electric-terminator) + ;;(define-key proof-mode-map (kbd coq-double-hit-hot-key) + ;; #'coq-terminator-insert) + (define-key map (kbd ".") #'coq-terminator-insert) + ;;(define-key map (kbd ";") #'coq-terminator-insert) ; for french keyboards + map)) + +;;;###autoload +(defun coq-pg-setup () + (set-keymap-parent (current-local-map) coq-pg-mode-map) + ;; coq-mode colorize errors better than the generic mechanism (setq proof-script-color-error-messages nil) (setq proof-terminal-string ".") @@ -1935,8 +1859,6 @@ Near here means PT is either inside or just aside of a comment." (setq proof-script-comment-start "(*") (setq proof-script-comment-end "*)") (setq proof-script-insert-newlines nil) - (set (make-local-variable 'comment-start-skip) "(\\*+ *") - (set (make-local-variable 'comment-end-skip) " *\\*+)") (setq proof-unnamed-theorem-name "Unnamed_thm") ; Coq's default name (setq proof-assistant-home-page coq-www-home-page) @@ -1948,7 +1870,7 @@ Near here means PT is either inside or just aside of a comment." ;; We manage file saveing via coq-compile-auto-save and for coq ;; it is not necessary to save files when starting a new buffer. (setq proof-query-file-save-when-activating-scripting nil) - + ;; Commands sent to proof engine (setq proof-showproof-command "Show. " proof-context-command "Print All. " @@ -1983,40 +1905,12 @@ Near here means PT is either inside or just aside of a comment." proof-nested-undo-regexp coq-state-changing-commands-regexp proof-script-imenu-generic-expression coq-generic-expression) - (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) - ;; (setq - ;; ;; indentation is implemented in coq-indent.el - ;; indent-line-function 'coq-indent-line - ;; proof-indent-any-regexp coq-indent-any-regexp - ;; proof-indent-open-regexp coq-indent-open-regexp - ;; proof-indent-close-regexp coq-indent-close-regexp) - ;; (make-local-variable 'indent-region-function) - ;; (setq indent-region-function 'coq-indent-region) - - - ;; span menu - (setq proof-script-span-context-menu-extensions 'coq-create-span-menu) + (setq proof-script-span-context-menu-extensions #'coq-create-span-menu) (setq proof-shell-start-silent-cmd "Set Silent. " proof-shell-stop-silent-cmd "Unset Silent. ") - (coq-init-syntax-table) - ;; we can cope with nested comments - (set (make-local-variable 'comment-quote-nested) nil) - - ;; font-lock - (setq proof-script-font-lock-keywords coq-font-lock-keywords-1) - - ;; FIXME: have abbreviation without holes - ;(if coq-use-editing-holes (holes-mode 1)) - (holes-mode 1) - ;; prooftree config (setq proof-tree-configured t @@ -2024,27 +1918,10 @@ Near here means PT is either inside or just aside of a comment." proof-tree-find-begin-of-unfinished-proof 'coq-find-begin-of-unfinished-proof) - (proof-config-done) - - ;; outline - (set (make-local-variable 'outline-regexp) coq-outline-regexp) - (set (make-local-variable 'outline-heading-end-regexp) - coq-outline-heading-end-regexp) - - ;; tags - (if (file-exists-p coq-tags) - (set (make-local-variable 'tags-table-list) - (cons coq-tags tags-table-list))) - - (set (make-local-variable 'blink-matching-paren-dont-ignore-comments) t) - - (when coq-may-use-prettify - (set (make-local-variable 'prettify-symbols-alist) - coq-prettify-symbols-alist)) - (setq proof-cannot-reopen-processed-files nil) - (add-hook 'proof-activate-scripting-hook #'proof-cd-sync nil t)) + (proof-config-done) + ) (defun coq-shell-mode-config () (setq @@ -2095,7 +1972,6 @@ Near here means PT is either inside or just aside of a comment." proof-shell-restart-cmd coq-shell-restart-cmd pg-subterm-anns-use-stack t) - (coq-init-syntax-table) ;; (holes-mode 1) da: does the shell really need holes mode on? (setq proof-shell-font-lock-keywords 'coq-font-lock-keywords-1) @@ -2120,7 +1996,7 @@ Near here means PT is either inside or just aside of a comment." proof-tree-show-sequent-command 'coq-show-sequent-command proof-tree-find-undo-position 'coq-proof-tree-find-undo-position ) - + (proof-shell-config-done)) @@ -2140,12 +2016,10 @@ Near here means PT is either inside or just aside of a comment." (defun coq-goals-mode-config () (setq pg-goals-change-goal "Show %s . ") (setq pg-goals-error-regexp coq-error-regexp) - (coq-init-syntax-table) (setq proof-goals-font-lock-keywords coq-goals-font-lock-keywords) (proof-goals-config-done)) (defun coq-response-config () - (coq-init-syntax-table) (setq proof-response-font-lock-keywords coq-response-font-lock-keywords) ;; The line wrapping in this buffer just seems to make it less readable. (setq truncate-lines t) @@ -2192,7 +2066,7 @@ Near here means PT is either inside or just aside of a comment." :type 'integer :setting "Set Printing Depth %i . ") -;;; Obsolete: +;; Obsolete: ;;(defpacustom undo-depth coq-default-undo-limit ;; "Depth of undo history. Undo behaviour will break beyond this size." ;; :type 'integer @@ -2309,7 +2183,7 @@ The not yet delayed output is in the region no-response-display proof-tree-show-subgoal)) proof-action-list)))))))))) - + (add-hook 'proof-tree-urgent-action-hook #'coq-proof-tree-get-new-subgoals) @@ -2330,7 +2204,7 @@ The not yet delayed output is in the region (span-property span 'goalcmd)) (span-start span) nil))) - + (defun coq-proof-tree-find-undo-position (state) "Return the position for undo state STATE. This is the Coq incarnation of `proof-tree-find-undo-position'." @@ -2621,7 +2495,7 @@ Based on idea mentioned in Coq reference manual." (defvar coq-keywords-accepting-as-regex (regexp-opt '("induction" "destruct" "inversion" "injection"))) ;; destruct foo., where foo is a name. -(defvar coq-auto-as-hack-hyp-name-regex +(defvar coq-auto-as-hack-hyp-name-regex (concat "\\(" "induction\\|destruct" "\\)\\s-+\\(" coq-id-shy "\\)\\s-*\\.") "Regexp of commands needing a hack to generate correct \"as\" close. tacitcs like destruct and induction reuse hypothesis names by @@ -2635,7 +2509,7 @@ Warning: this makes the error messages (and location) wrong.") (defun coq-hack-cmd-for-infoH (s) "return the tactic S hacked with infoH tactical." (cond - ((string-match ";" s) s) ;; composed tactic cannot be treated + ((string-match ";" s) s) ;; composed tactic cannot be treated ((string-match coq-auto-as-hack-hyp-name-regex s) (concat "infoH " (match-string 1 s) " (" (match-string 2 s) ").")) ((string-match coq-keywords-accepting-as-regex s) @@ -2792,7 +2666,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (define-key coq-keymap [(control ?q)] 'coq-query) (define-key coq-keymap [(control ?r)] 'coq-insert-requires) ; [ for "as [xxx]" is easy to remember, ccontrol-[ would be better but hard to type on french keyboards -; anyway company-coq should provide an "as!<TAB>". +; anyway company-coq should provide an "as!<TAB>". (define-key coq-keymap [(?\[)] 'coq-insert-as-in-next-command) ;; not for goal/response buffer? ; Query commands @@ -2882,13 +2756,13 @@ Completion is on a quasi-exhaustive list of Coq tacticals." ;; Default binding: clicking on the cross to folds/unfold hyp. ;; Click on it with button 2 copies the names at current point. -(when coq-hypname-map +(when coq-hypname-map (define-key coq-hypcross-map [(mouse-1)] 'coq-toggle-fold-hyp-at-mouse) (define-key coq-hypcross-map [return] 'coq-toggle-fold-hyp-at-point) (define-key coq-hypcross-map [(mouse-2)] 'coq-insert-at-point-hyp-at-mouse)) ;; Ddefault binding: clicking on a hidden hyp with button 3 unfolds it, with ;; button 2 it copies hyp name at current point. -(when coq-hidden-hyp-map +(when coq-hidden-hyp-map (define-key coq-hidden-hyp-map [(mouse-3)] 'coq-toggle-fold-hyp-at-mouse) (define-key coq-hidden-hyp-map [(mouse-2)] 'coq-insert-at-point-hyp-at-mouse)) @@ -2979,7 +2853,7 @@ buffer." (lgth (cadr mtch))) (goto-char (+ (proof-unprocessed-begin) 1)) (coq-find-real-start) - + ;; utf8 adaptation is made in coq-get-last-error-location above (let ((time-offset (if coq-time-commands (length coq--time-prefix) 0))) (goto-char (+ (point) pos)) @@ -3126,7 +3000,7 @@ Only when three-buffer-mode is enabled." ;; https://github.com/cpitclaudel/company-coq/issues/8. (unless (memq 'no-response-display proof-shell-delayed-output-flags) ;; If there is no frame with goql+response then do nothing - (when proof-three-window-enable + (when proof-three-window-enable (let ((threeb-frames (coq-find-threeb-frames))) (when threeb-frames (let ((pg-frame (car threeb-frames))) ; selecting one adequate frame @@ -3149,7 +3023,7 @@ Only when three-buffer-mode is enabled." (goto-char (point-min)) (recenter))))))))))))) -;; TODO: remove/add hook instead? +;; TODO: remove/add hook instead? (defun coq-optimise-resp-windows-if-option () (when coq-optimise-resp-windows-enable (coq-optimise-resp-windows))) @@ -3200,7 +3074,7 @@ It will be restored if double hit terminator is toggle off.") ;; We redefine the keybinding when we go in and out of double hit mode, even if ;; in principle coq-terminator-insert is compatible with -;; proof-electric-terminator. This may be overprudent but I suspect that +;; proof-electric-terminator. This may be overprudent but I suspect that (defun coq-double-hit-enable () "Disables electric terminator since double hit is a replacement. This function is called by `proof-set-value' on `coq-double-hit-enable'." @@ -3216,8 +3090,6 @@ This function is called by `proof-set-value' on `coq-double-hit-enable'." -;;(define-key coq-mode-map coq-double-hit-hot-key 'coq-terminator-insert) - (proof-deftoggle coq-double-hit-enable coq-double-hit-toggle) (defadvice proof-electric-terminator-enable (after coq-unset-double-hit-advice) @@ -3279,18 +3151,11 @@ priority to the former." (put 'coq-terminator-insert 'delete-selection t) -;; Setting the new mapping for terminator, overrides the following in proof-script: -;; (define-key proof-mode-map (vector (aref proof-terminal-string 0)) 'proof-electric-terminator) - -;(define-key proof-mode-map (kbd coq-double-hit-hot-key) 'coq-terminator-insert) -(define-key coq-mode-map (kbd ".") 'coq-terminator-insert) -;(define-key coq-mode-map (kbd ";") 'coq-terminator-insert) ; for french keyboards - ;;;;;;;;;;;;;; ;; This was done in coq-compile-common, but it is actually a good idea even ;; when "compile when require" is off. When switching scripting buffer, let us -;; restart the coq shell process, so that it applies local coqtop options. +;; 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 t) |