aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
Commit message (Collapse)AuthorAge
* Derive proof-mode from prog-modeHEADmasterGravatar Benjamin Barenblat2019-04-18
| | | | | | | | | | prog-mode [1] is the base mode for programming that comes with Emacs: “All major modes for programming languages should derive from this mode so that users can put generic customization on prog-mode-hook.” Make proof-mode derive from prog-mode, reflecting its status as a programming mode. [1] https://git.savannah.gnu.org/cgit/emacs.git/tree/lisp/progmodes/prog-mode.el?id=a18336a8dc754fa1c68e16dd8009466cf409271b
* * pg-init.el: Add subdirs during compilation (bug #413)Gravatar Stefan Monnier2019-01-12
| | | | | * generic/pg-user.el (proof-add-completions): `proof-assistant` can also be the empty string :-(
* 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.
* Reduce the impact of proof-site, in case PG is not usedGravatar Stefan Monnier2018-12-25
| | | | | | | | | | | | | | | | * generic/proof-autoloads.el: Remove `require`s; not needed. * generic/proof-site.el: Don't require `pg-vars`. (proof-ready-for-assistant): Move to proof-script.el. * generic/proof-menu.el (proof-assistant-format): Make dynamically scoped var explicit (preparation for lexical-binding). * generic/proof-script.el: Require `pg-vars`. (proof-ready-for-assistant): Move from proof-site.el. * generic/proof-syntax.el (proof-replace-regexp-in-string): * generic/proof-shell.el (proof-shell-live-buffer): Don't mark it as inlinable: it's not performance sensitive.
* * 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.
* 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
* Fix remaining uses of CL; Make files more declarativeGravatar Stefan Monnier2018-12-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Emacs occasionally loads Elisp files just to get more info (e.g. for C-h f), so loading a file should "no effect". Fix the most obvious such effects: the splash screen and the autotests by moving those effects into a function. * coq/coq-autotest.el: Make it declarative. Use lexical-binding. (coq-autotest): New function holding the code that used to be at top-level. * generic/proof.el: Use lexical-binding. Don't call proof-splash-message just because we're being loaded. * generic/proof-script.el: Use lexical-scoping; fix all warnings. (pg-show-all-portions): Simplify the code with a closure. (proof-activate-scripting): Declare activated-interactively as dyn-scoped. (proof--splash-done): New var. (proof-mode): Call proof-splash-message upon first use. * generic/proof-splash.el (proof-splash-message): Don't check byte-compile-current-file now that we're only called when the mode is activated. * acl2/acl2.el (auto-mode-alist): Use `add-to-list` and \'. * coq/coq-db.el (coq-build-menu-from-db-internal): Avoid silly O(N²). * coq/coq-seq-compile.el: * coq/coq-par-test.el: * coq/coq-par-compile.el: Fix leftover uses of CL's `assert`. * generic/proof-utils.el: * generic/pg-movie.el: * etc/testsuite/pg-test.el: * coq/coq-syntax.el: Fix leftover uses of CL's `incf`. * generic/pg-autotest.el: Fix leftover uses of CL's `decf`. * obsolete/plastic/plastic.el (plastic-preprocessing): Fix leftover use of CL's `loop`. * generic/pg-user.el (proof-add-completions): Do nothing if no proof-assistant is set yet (i.e. during byte-compilation). (byte-compile-current-file): No need to test this any more. * generic/proof-syntax.el (proof-regexp-alt-list): Use mapconcat. Remove unnecessary "\\(?:...\\)". (proof-regexp-alt): Redefine in terms of proof-regexp-alt-list.
* Fixes the fix of #407. Is this temporary.Gravatar Pierre Courtieu2018-12-14
| | | | | | | | | | | | | | This fix is not completely satisfying for the following reason: 1- I had to add a new hook in generic code. But I don't see how we could avoid this: the computation of options must happen AFTER the proof-prog-name is asked to the user, because this computation depends on the version of coq. 2- We should fix the synchronization between coq-prog-name and proof-prog-name. Either remove coq-prog-name and use only proof-prog-name, or have the generic coq always point to some (proof-ass-sym prog-name).
* 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.
* Remove code that hides mode-line.Gravatar Calvin Beck2018-11-12
|
* Reloading proof-autoloads is safe; don't forbid itGravatar Clément Pit-Claudel2018-09-01
| | | | | | Fixes GH-386. Reported-by: @mrkkrp
* Merge pull request #169 from ProofGeneral/help-span-extendedGravatar Erik Martin-Dorel2018-08-25
|\ | | | | Fix #158 by extending helpspan
* | Run make autoloadsGravatar Erik Martin-Dorel2018-08-23
| |
* | Fix most doc issues raised by (checkdoc)Gravatar Erik Martin-Dorel2018-08-23
| |
* | Bump version from 4.4.1~pre to 4.5-gitGravatar Erik Martin-Dorel2018-08-22
| | | | | | | | This commit ensures the version number is (version-to-list)-compliant.
* | Merge pull request #200 from craff/masterGravatar Erik Martin-Dorel2018-08-22
|\ \ | | | | | | Update phox support
* | | Add a missing parameter in advice on font-lock-fontify-keywords-regionGravatar Clément Pit--Claudel2018-03-07
| | |
* | | Update copyright messages and improve the header of elisp files.Gravatar Erik Martin-Dorel2018-02-21
| | |
* | | Bind C-c C-m (= C-c RET) to proof-goto-point [tty] (#228)Gravatar Erik Martin-Dorel2018-02-20
| | | | | | | | | Close ProofGeneral/PG#31
| * | phox is backGravatar Christophe Raffalli2017-09-22
|/ /
* | Fix pg-{show,hide}-all-proofs and Move them into pg-user.el.Gravatar Erik Martin-Dorel2017-08-15
| | | | | | | | This commit address ProofGeneral/PG#193.
* | Fix easycrypt automode regexpGravatar Mario Rodas2017-06-19
| | | | | | | | | | Without the string-end regexp matches all the file names which match the regexp `.eca?`.
* | Fixing bug #187 by removing trailing spaces from prog name.Gravatar Pierre Courtieu2017-06-06
| |
* | Remove mmm and ML4PG contribs and remove references to them in code and docsGravatar Paul Steckler2017-05-24
| |
* | 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
* | | Fixing #167.Gravatar Pierre Courtieu2017-03-13
| | |
| | * extend helpspan, issue #158Gravatar Paul Steckler2017-03-09
| |/ |/|
| * Remove uses of defpgdefault in coq-abbrevGravatar Clément Pit--Claudel2017-03-08
| | | | | | | | | | | | This file is `require'-d when compiling coq.el, and at that point the proof assistant isn't set to coq yet, so it would define variables prefixed by `nil-' instead of `coq'.
| * 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
| |
| * Remove some Emacs <24.1 compatibility cruftGravatar 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.
| * Fix incorrect assumption that noninteractive == byte-compilingGravatar Clément Pit--Claudel2017-03-08
|/ | | | | The PG Makefile does ensure (using --batch) that noninteractive is non-nil while compiling, but package.el doesn't.
* Merge pull request #163 from ProofGeneral/fix_indentationGravatar Pierre Courtieu2017-03-03
|\ | | | | Fix indentation
* | Remove default key-binding for proof-electric-terminator-toggle.Gravatar Erik Martin-Dorel2017-03-03
| | | | | | | | Close ProofGeneral/PG#160
* | Removing spurious debug messages.Gravatar Pierre Courtieu2017-02-24
| |
* | Fixing #154.Gravatar Pierre Courtieu2017-02-23
| |
| * Merge branch 'master' of github.com:ProofGeneral/PG into master_originGravatar Pierre Courtieu2017-01-26
| |\ | |/ |/|
| * annoying missing parentheisis in a comment.Gravatar Pierre Courtieu2017-01-24
| |
* | 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
* | split emergency-cleanup to handle interrupts properly (fixes #143)Gravatar Hendrik Tews2017-01-18
| | | | | | | | | | | | Split coq-par-emergency-cleanup into two functions, one for reacting on user interrupts and one for cleaning up after compilation errors.
* | move phox from main to obscure instancesGravatar Hendrik Tews2017-01-17
| | | | | | | | | | see http://proofgeneral.inf.ed.ac.uk/trac/ticket/434, when I tried to download phox now, no link was working...
* | Merge pull request #44 from EasyCrypt/masterGravatar hendriktews2017-01-17
|\ \ | | | | | | EasyCrypt PG mode
* | | 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.
* | Merge remote-tracking branch 'OFFICIAL/master'Gravatar Pierre Courtieu2017-01-04
|\ \
* | | Fixing #121 + avoid hiding user windows too much.Gravatar Pierre Courtieu2017-01-04
| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-29 15:06:55 +0000