| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
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 #158 by extending helpspan
|
|
|
|
|
|
This commit address ProofGeneral/PG#193.
|
|
|
|
Close ProofGeneral/PG#160
|
|
|
|
Fixes #65
|
|
proof-script-buffer was not set before calling proof-shell-ready-prover.
|
|
|
|
This hook was missing, it allows to send complete commands before
the (set of) command(s) sent by the user. It shall be used when
proof-shell-insert-hook cannot be used (because of multiple prompts
appearing).
|
|
|
|
|
|
|
|
* generic/proof-site.el (assistants): Fix regexp.
|
|
comment-start-skip: if it is already set then proof-script should not
change it. Ultimately if David approves we should moreover fix the
setting itself which is bugged.
coq-mode now sets this variable by itself.
|
|
interactive-p with called-interactively-p)
|
|
|
|
coq-compile-response-buffer
- fix typo elsewhere
|
|
avoid hitting read only error in calling command.
|
|
|
|
removing restriction during automatic retraction so
proof-retract-until-point behaves correctly.
|
|
|
|
proof-last-edited-low-watermark.
|
|
http://proofgeneral.inf.ed.ac.uk/trac/ticket/395
|
|
proof-shell-require-command-regexp
- TAGS updated to really flush them
|
|
|
|
who read or edit by waving mouse at text
|
|
- improve internal docs for unlocking
|
|
|
|
intelligible, also to properly support behaviour needed for
`proof-no-fully-processed-buffer'.
|
|
now a list of functions to be run when the span is deleted. Use
span-add-delete-action to add a delete action.
|
|
Addresses Trac #383
|
|
|
|
- add documentation for it
- add a test case demonstrating it in
coq/ex/test-cases/retract-completely-asserted
|
|
The following points are implemented already:
- recompile either via an external command (make) or let
ProofGeneral handle everything internally
- complete dependency tracking and recompilation for coq files in
internal mode
- support for extending the LoadPath: does almost work, even if
specified file-locally
- move back to clean state if recompilation fails
There are the following known problems:
- coq-load-path extensions are not retracted
- fails on partially qualified library names
|
|
|
|
|
|
proof-complete-buffer-atomic: simplify.
Add debug message for parser cache.
|
|
|
|
after it as well as before,
as in PG 3.7. Fixes #371.
|
|
|
|
input (no non-nil flags in queue)
|
|
|
|
|
|
|
|
|
|
span regions.
|
