| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
| |
This commit ensures the version number is (version-to-list)-compliant.
|
| |\
| |
| | |
Update phox support
|
| | | |
|
| |/ |
|
| |
|
|
|
| |
Without the string-end regexp matches all the file names which match the regexp
`.eca?`.
|
| |
|
|
|
|
|
| |
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.
|
| |
|
|
|
| |
see http://proofgeneral.inf.ed.ac.uk/trac/ticket/434, when I
tried to download phox now, no link was working...
|
| |\
| |
| | |
EasyCrypt PG mode
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| | |
The new art is a contribution of Yoshihiro Imai
(http://proofcafe.org/~yoshihiro503/), first released at
https://github.com/yoshihiro503/generaltan and kindly made available
under the terms of the GPL. Many thanks!
|
| | | |
|
| |/ |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
* generic/proof-site.el (assistants): Fix regexp.
|
| | |
|
| |
|
|
|
| |
distributions with specific requirements (such as Debian with
debian-pkg-add-load-path-item) only need to patch one function.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
Stefan Monnier
Erik Martin-Dorel
Christophe Raffalli
Mario Rodas
Clément Pit--Claudel
Hendrik Tews
Pierre-Yves Strub
David Aspinall