aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq.el
Commit message (Collapse)AuthorAge
* Make coq-mode work without generic/proof-*Gravatar Stefan Monnier2018-12-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Revise the various `require`s to avoid spurious dependencies, and tweak the code here and there to eliminate the remaining dependencies. * coq/coq-db.el: Don't require proof-config nor proof-syntax. (coq-build-opt-regexp-from-db): Avoid proof-regexp-alt-list. * coq/coq-indent.el: Use lexical-binding. Don't require coq-syntax. Comment out all the code that's not used any more. (coq-empty-command-p): Use forward-comment instead of coq-find-not-in-comment-backward. Fix paren typos. (coq-script-parse-cmdend-forward, coq-script-parse-cmdend-backward): Use forward-comment i.s.o proof-script-generic-parse-find-comment-end. Use syntax-ppss i.s.o proof-buffer-syntactic-context. (coq-find-current-start): Explicit case-fold-search i.s.o proof-looking-at. * coq/coq-mode.el (coq-mode): Set comment-start/end. * coq/coq-smie.el: Require coq-syntax explicitly. (coq-smie-detect-goal-command, coq-smie-module-deambiguate): Explicit case-fold-search i.s.o proof-looking-at. (coq-indent-basic): New custom var. (coq-smie-rules): Use it in case PG is not loaded. * coq/coq-syntax.el: Don't require proof-syntax, proof-utils, and span. (coq-goal-command-p): Use overlay-get i.s.o span-property. (coq-save-command-regexp-strict, coq-save-command-regexp): Use \` and regexp-opt i.s.o proof-anchor-regexp and proof-ids-to-regexp. (coq-save-command-p): Explicit case-fold-search i.s.o proof-string-match. (coq--regexp-alt-list-symb): Rename from proof-regexp-alt-list-symb. Use mapconcat i.s.o proof-regexp-alt-list. (coq-save-with-hole-regexp): Use regexp-opt i.s.o proof-regexp-alt-list. (coq-goal-command-regexp, coq-goal-with-hole-regexp) (coq-decl-with-hole-regexp, coq-defn-with-hole-regexp) (coq-font-lock-keywords-1): Use mapconcat i.s.o proof-regexp-alt-list. (coq-find-first-hyp, coq-detect-hyps-positions-in-goals): Use current buffer i.s.o proof-goals-buffer. (coq-with-altered-syntax-table): Fix broken use of unwind-protect. * coq/coq.el (coq-detect-hyps-in-goals): Change buffer before calling coq-find-first-hyp and coq-detect-hyps-positions-in-goals. (coq-pg-setup): Use comment-start/end. * generic/pg-goals.el: Require proof-script explicitly instead of autoloading via proof-insert-sendback-command. * generic/pg-pbrpm.el: Require proof-script explicitly instead of autoloading via proof-insert-pbp-command. * generic/pg-pgip.el: Require proof-script explicitly. * generic/proof-depends.el: Require proof-script explicitly instead of autoloading via pg-set-span-helphighlights. * generic/proof-script.el (pg-set-span-helphighlights) (proof-insert-pbp-command, proof-insert-sendback-command) (proof-script-generic-parse-find-comment-end): Don't autoload. * generic/proof-syntax.el (proof-ids-to-regexp): Simplify. * lib/span.el (span-delete): η-reduce.
* * coq-mode.el: New file to make coq-mode independent from PGGravatar Stefan Monnier2018-12-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Move the part of coq.el that is not specific to ProofGeneral into coq-mode.el to make `coq-mode` into a major mode that can work without PG. * coq/coq-mode.el: New file, with code extracted from coq.el. (coq-use-pg): New var. (coq-near-comment-region): Complete rewrite. * Makefile.devel (autoloads): Add `coq` to the scanned subdirectories. * generic/proof-autoloads.el: Regenerate. * generic/proof-site.el: Don't override pre-existing major-mode definitions. * coq/coq-syntax.el (coq-init-syntax-table): Delete function. Setup the syntax-table while loading coq-mode.el instead. * coq/coq-system.el (coq-prog-name, get-coq-library-directory) (coq-library-directory, coq-tags): Move to coq-mode.el. * coq/coq.el: Set proof-assistant when loaded. (coq-may-use-prettify, coq-outline-regexp) (coq-outline-heading-end-regexp, coq-mode) (coq-prettify-symbols-alist, coq-fill-paragraph-function) (coq-adaptive-fill-function): Move to coq-mode.el. (coq-shell-mode-syntax-table, coq-response-mode-syntax-table) (coq-goals-mode-syntax-table): Just reuse the already setup coq-mode-syntax-table... (coq-shell-mode-config, coq-goals-mode-config, coq-response-config): ... instead of calling coq-init-syntax-table. (coq-get-comment-region): Delete, not used any more. (coq-pg-mode-map): New var. Move top-level keymap setup here. (coq-pg-setup): Rename from coq-mode-config. Move all the non-PG specific settings to coq-mode. * generic/proof-script.el (proof-mode): Simplify call to proof-splash-message since it does the same extra tests internally. (proof-config-done-related): Don't touch font-lock-defaults if the mode doesn't provide any font-lock-defaults. * isar/isar-syntax.el: Use lexical-binding. (isar-font-lock-fontify-syntactically-region): Make it callable from font0lock-keywords. (isar-font-lock-keywords-1): Call isar-font-lock-fontify-syntactically-region. * generic/proof-syntax.el (font-lock-fontify-keywords-region): Remove advice. (proof-ids): Remove, unused. * lib/bufhist.el (bufhist-erase-buffer): Don't let-bind after-change-functions. * generic/pg-pbrpm.el (pg-pbrpm-auto-select-around-point): Fix one more left-over cl.el use. * generic/proof-utils.el (proof-with-script-buffer): Add edebug spec.
* Merge branch 'master' of github.com:ProofGeneral/PGGravatar Pierre Courtieu2018-12-20
|\
* | Fixes #395: hyps highlight is transient and with gray background.Gravatar Pierre Courtieu2018-12-20
| |
| * Quote ?( ?)Gravatar soraros2018-12-19
| |
| * Cosmetic cleanup of coq-smie, coq-syntax, and coq-abbrev.Gravatar Stefan Monnier2018-12-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fix a few more cl.el leftovers. Get rid of remaining use of iso-2022. Use SMIE unconditionally. * coq/coq-abbrev.el: Use lexical-binding. (coq-install-abbrevs): Delete, only keep the relevant contents. (proof-defstringset-fn): Remove. Fold changes into the main version. * coq/coq-indent.el (coq-find-real-start): Use forward-comment. * coq/coq-smie.el: Use lexical-binding. Assume `smie` is available. (coq--string-suffix-p): Rename from coq-string-suffix-p. Use string-suffix-p for it when available. (string-suffix-p): Never define here. Change all users to use coq--string-suffix-p instead. (coq-smie-.-deambiguate): Use forward-comment. Remove unused var `beg`. (coq-backward-token-fast-nogluing-dot-friends) (coq-forward-token-fast-nogluing-dot-friends): Remove unused var `tok-other`. (coq-smie-search-token-backward): Remove unused var `p`. (coq-smie-:=-deambiguate, coq-smie-backward-token): Prefer char-before over looking-back. (coq-smie-rules): Use `pcase` over deprecated cl's `case`. * coq/coq-syntax.el: Use lexical-binding. (coq-count-match): Rewrite so it doesn't do needless heap-allocation. (coq-module-opening-p, coq-section-command-p, coq-goal-command-str-p): Use case-fold-search rather than proof-string-match. (coq-goal-command-regexp): Forward-declare. (coq-save-command-regexp-strict): Move before first use. (coq-reserved-regexp): Use a single \_< ... \_>. (coq-detect-hyps-positions): Limit search for looking-back. * coq/coq.el: Remove SMIE declarations since SMIE is always used. (coq-use-smie): Remove, unused. (coq-smie): Always require. * generic/pg-pbrpm.el: Fix leftover cl.el uses. * generic/proof-utils.el (proof-defstringset-fn): Fix copy&paste error in the docstring, improve interactive prompt. * lib/maths-menu.el: Use utf-8 and lexical-binding.
| * Prepend cl- to more c[ad]+r instancesGravatar Clément Pit-Claudel2018-12-15
| |
| * Use cl-caddr instead of caddrGravatar Clément Pit-Claudel2018-12-15
|/ | | | | | Hopefully fixes #409. Reported-By: @lysxia
* Use `cl-lib` instead of `cl` everywhereGravatar Stefan Monnier2018-12-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Use lexical-binding in a few files where it was easy. Don't require `proof-compat` when it's not used. * coq/coq-db.el: Use lexical-binding. * coq/coq-system.el: Use lexical-binding. (coq--extract-prog-args): Use concatenated-args rather than recomputing it. * coq/coq.el: Require `span` to silence some warnings. * generic/pg-user.el: Use lexical-binding. (complete, add-completion, completion-min-length): Silence warnings. * generic/pg-xml.el: Use lexical-binding. (pg-xml-string-of): Prefer mapconcat to reduce+concat. * generic/proof-depends.el: Use lexical-binding. (proof-dep-split-deps): Use `push`. * generic/proof-shell.el: Require `span` to silence some warnings. (proof-shell-invisible-command): Don't use lexical-let just to build a wasteful η-redex! * lib/holes.el: Use lexical-binding. Remove redundant :group args. * lib/span.el: Use lexical-binding. (span-read-only-hook): Use user-error. (span-raise): Remove, unused.
* Cleanup patch; Moving defvar to toplevelGravatar Stefan Monnier2018-12-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Move `defvar`s used to silence warnings outside of eval-when-compile. Make sure they don't actually give a value to the var. * pg-init.el: Simplify. Use (if t ...) to avoid running `require` at compile-time. Don't add subdirs to load-path here since this code is never used. (pg-init--script-full-path, pg-init--pg-root): Inline their definition into their sole user. * generic/proof-utils.el (proof-resize-window-tofit): Inline definitions of window-leftmost-p and window-rightmost-p previously in proof-compat.el. * lib/proof-compat.el (proof-running-on-win32): Remove, not used. (mac-key-mode): Remove, there's no carbon-emacs-package-version in Emacs≥24.3. (pg-custom-undeclare-variable): Use dolist. (save-selected-frame): Remove, save-selected-window also saves&restores the selected frame at the same time. Update all users (which already used save-selected-window around it). (window-leftmost-p, window-rightmost-p, window-bottom-p) (find-coding-system): Remove, unused. * hol-light/hol-light.el (caml-font-lock-keywords): Don't try to defvar it to a dummy value and... (hol-light): ...check its existence before using it instead. * coq/coq.el (coq-may-use-prettify): Simplify initialization.
* Fix most doc issues raised by (checkdoc)Gravatar Erik Martin-Dorel2018-08-23
|
* Add coq-Print-Ltac to print an Ltac termGravatar John Grosen2018-08-07
|
* small fix on hyp overlays.Gravatar Pierre Courtieu2018-06-13
|
* Fix multiple hyp overlays.Gravatar Pierre Courtieu2018-06-13
| | | | | queries would trigger re-generarion of overlays. Now overlays are generated if there are no overlays already.
* Fix the fix #355.Gravatar Pierre Courtieu2018-06-13
| | | | The fix was bad: no ore hyps were foldable/highlightable.
* Small bug unhighlighting.Gravatar Pierre Courtieu2018-06-11
| | | | | Selecting the unhighlightied hyps showed a different region color. Setting the face to nil is better.
* key maps + small glitch hyp highlight/folding code.Gravatar Pierre Courtieu2018-06-11
|
* Changed the look of folding/unfolding hyps.Gravatar Pierre Courtieu2018-06-08
|
* Shorter CHANGES + smal fixes in hide/highlight hyps code.Gravatar Pierre Courtieu2018-06-04
|
* Click hypothesis to (un)hide them.Gravatar Pierre Courtieu2018-06-01
|
* Fixed a typo in previous commits.Gravatar Pierre Courtieu2018-06-01
|
* Infrastructure for hypothesis hiding.Gravatar Pierre Courtieu2018-05-31
|
* Fixing infrastructure for hypothesis highlighting.Gravatar Pierre Courtieu2018-05-31
|
* Infrastructure for transient hyps highlighting.Gravatar Pierre Courtieu2018-05-31
|
* Fix typos in custom variable descriptions. (#236)Gravatar Tej Chajed2018-03-03
|
* Update copyright messages and improve the header of elisp files.Gravatar Erik Martin-Dorel2018-02-21
|
* Fix #214.Gravatar Pierre Courtieu2017-12-11
| | | | If this works we should probably change the generic function as well.
* Fixing a bug with Set/Unset commands due to recent commits.Gravatar Pierre Courtieu2017-06-08
| | | | | The "Show" inserted now and then would hide the result of Set/Unset commands.
* Adding a Set Silent + Show when backtracking into a proof.Gravatar Pierre Courtieu2017-06-06
| | | | | Checking whether the backtrack is inside a proof or not is a bit convoluted but seems ok.
* Remove mmm and ML4PG contribs and remove references to them in code and docsGravatar Paul Steckler2017-05-24
|
* Fixing Set/Unset Printing broken by auto "Show".Gravatar Pierre Courtieu2017-05-16
| | | | | | Current coq trunk has a bug with Show that I reported (there is a spurious Show executed) which makes C-u C-c C-a C-s fail for now. Should be fixed shortly.
* temporary fix of automatic intros.Gravatar Pierre Courtieu2017-05-12
|
* Change (eval-when (compile) ...) to (eval-when-compile ...)Gravatar Clément Pit--Claudel2017-05-05
| | | | This fixes a bunch of compilation warnings
* Merge pull request #157 from ProofGeneral/elpaGravatar Clément Pit-Claudel2017-05-05
|\ | | | | [WIP] ELPA/MELPA support
* | Preparing new warning tags (no more special chars).Gravatar Pierre Courtieu2017-04-24
| |
* | Added support for future new options (trunk).Gravatar Pierre Courtieu2017-03-22
| |
| * Add a FIXME in coq.elGravatar Clément Pit--Claudel2017-03-08
| |
| * Remove compile-time calls to proof-ready-for-assistantGravatar Clément Pit--Claudel2017-03-08
| | | | | | | | | | Compilation used to run in a separate Emacs process for each file, but that's not what happens when installing PG with package.el.
| * Remove unnecessary calls to 'eval-and-compile'Gravatar Clément Pit--Claudel2017-03-08
| |
| * Fix incorrect uses of defvarGravatar Clément Pit--Claudel2017-03-08
|/ | | | | | | It didn't really matter that these variables were defined and set to nil during compilation, since we ran compilation in a clean Emacs in --batch mode; it does matter now, however, since package.el compiles PG in the user's currently running Emacs instance.
* get threeb frames only when neededGravatar Paul Steckler2017-03-06
|
* one more redundant call removedGravatar Paul Steckler2017-03-06
|
* remove redundant calls, simplify codeGravatar Paul Steckler2017-03-06
|
* Refreshing goal when Set Printing xxx. (#162)Gravatar Pierre Courtieu2017-03-03
| | | | | * Close ProofGeneral/PG#161. Issue a "Show" each time a (Uns|S)et Printing is detected (and a proof is open).
* Fixing #154.Gravatar Pierre Courtieu2017-02-23
|
* save settings not defined with defpacustom (fixes #142)Gravatar Hendrik Tews2017-01-19
| | | | | | | - infrastructure for saving/resetting customizations not defined with defpacustom - improve Coq -> Auto Compilation menu - polish documentation and manual
* Fix prooftree for Coq 8.6Gravatar Hendrik Tews2017-01-14
| | | | | | | In Coq 8.6 evar status printing is off by default, causing prooftree to crash. This patch inserts invisible commands to switch evar status printing on and off. This is done via the urgent-action-hook.
* add second argument to looking-back, required in emacs25Gravatar Hendrik Tews2016-12-31
|
* properly reset the vio2vo delay timerGravatar Hendrik Tews2016-12-28
| | | | | cancel-timer does of course not set the variable that holds the timer to nil
* add quote to fix commit e3cc66dc2e60683531d75c12256d059ccbc64576Gravatar Hendrik Tews2016-12-15
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 01:11:48 +0000