| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
Make proof-goto-point and proof-process-buffer prefix argument
aware. With argument, both commands temporarily switch off
proof-omit-proofs-option, such that all proofs are completely
processed for one particular invocation.
|
|
Closes GH-557.
|
|
* Document (in README.md) the proposed policy: supporting Emacsen from
the versions packaged in Debian Stable / Ubuntu LTS until their EOS.
|
|
|
|
|
|
|
|
In 7389d43893569ff0e1eff892254901876fc8225e
proof-ready-for-assistant was moved to proof-script.el, breaking
make magic in a complicated chain. The auto load for
proof-ready-for-assistant caused proof-script.el to be loaded
before proof-assistant was set, causing
proof-eval-when-ready-for-assistant, to put stuff into
proof-ready-for-assistant-hook. proof-ready-for-assistant loads
pg-custom.el by require, therefore, for the first proof assistant
in the loop in docstring-magic everything was defined when
executing the hooks at the end of proof-ready-for-assistant. The
second assistant caused errors than.
Fixes #542
|
|
this problem was introduced in a921439a4eb5b0d96182748e779c78e2f6a41a5f
|
|
proof-state-change-pre-hook happens earlier than
proof-state-change-hook, i.e. before proof-done-advancing. This should
be used to register information in the currently processed span before
proof-done-advancing classifies it.
Historically PG design was to gather these information during
proof-done-advancing (or in its hook called at the end) by just
looking at the command statement. But it is often useful to look at
the output (messages and/or prompt) to gather more accurate
information. Some of this information may be needed DURING
proof-done-advancing. Hence this early hook.
|
|
Fixes the following error:
node `Coq Proof General' lacks menu item for `Proof using annotations' despite being its Up target
|
|
|
|
|
|
Note that currently, there is no keybinding associated to the electric
terminator.
|
|
|
|
|
|
This a generalization of PR#451 proposed by @Chobbes.
Since these syntax are not completely universal (and not builtin in
coq), the idea is to make the syntax customizable, especially to make
it possible to disable it.
NOTE: to make the Compcert syntax supported I had to refine the smie
lexer so that the ";" token was emitted as a fllback instead of ";
tactic".
NOTE2: I had to make the coq-user-token and coq-monadic-tokens be
tested ON THE RESULT of smie-coq-backward-token.
|
|
context (with diff annotations when enabled).
|
|
using Coq's proof diffs feature.
|
|
|
|
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.
|
|
|
|
|
|
|
|
This commit ensures the version number is (version-to-list)-compliant.
|
|
This agrees with the minimal version of GNU Emacs currently tested by
Travis CI, as well as with the version packaged in Ubuntu 14.04 LTS
Reference:
https://github.com/ProofGeneral/PG/issues/368#issuecomment-397561986
|
|
|
|
|
|
|
|
|
|
- infrastructure for saving/resetting customizations not defined
with defpacustom
- improve Coq -> Auto Compilation menu
- polish documentation and manual
|
|
texi2html is dead, see for instance
https://wiki.debian.org/Texi2htmlTransition
|
|
Close ProofGeneral/PG#138.
|
|
... following the discussion in github on 32fea19d1bb66593e469b1a8e6ad38f3ae1714bf
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
