| Age | Commit message (Collapse) | Author |
|---|
|
This commit adds a feature to recognize complete opaque proofs in
the asserted region and to replace them with an admitted proof.
This can drastically improve the processing time for the asserted
region at the cost of not checking the omitted proofs. Omitted
proofs are displayed slightly darker compared to other parts of
the locked region.
With this commit, the feature is supported for Coq for files in
which proofs are started with some form of Proof and ended with
either Qed, Defined, Admitted or Abort.
To enable, configure proof-omit-proofs-option or click
Proof General -> Quick Options -> Processing -> Omit Proofs.
|
|
* require package.el (in a safe way thanks to `proof-try-require`)
|
|
Backported those typos that were fixed only in the manual texi
sources and not in the doc strings, from which the text was
imported. Convert a few symbols quoted with curved unicode single
quotations to ascii, such that make magic recognizes them.
|
|
This patch allows one to load the `coq-diffs' option at Coq startup,
provided the ambient Coq version is >= 8.10.
This additional "lambda" format is needed because [Set Diffs "on".] is neither:
- a boolean setting from Coq side (there are three possible values)
- a string setting from Emacs side (it is implemented as a radio/symbol option)
- a cross-version compatible Coq setting.
|
|
using Coq's proof diffs feature.
|
|
* 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.
|
|
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.
|
|
Hopefully fixes #409.
Reported-By: @lysxia
|
|
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.
|
|
|
|
|
|
Close ProofGeneral/PG#31
|
|
|
|
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.
|
|
- infrastructure for saving/resetting customizations not defined
with defpacustom
- improve Coq -> Auto Compilation menu
- polish documentation and manual
|
|
|
|
|
|
- add support for proof-tree displays (currently Coq only)
- new file generic/proof-tree.el contains generic code
- Coq specific code has been added to coq/coq.el
Changes to existing Proof General functions:
- proof-shell-exec-loop and proof-shell-filter-manage-output call
proof-tree display functions, when the proof-tree display is on
- proof-shell-exec-loop returns t if proof-action-list is empty
_or_ contains only items for updating the proof-tree
- proof-shell-should-be-silent returns nil when the proof-tree
display is on
- coq-last-prompt-info, coq-last-prompt-info-safe return as
additional 4th element the name of the current proof
|
|
interactive-p with called-interactively-p)
|
|
|
|
Emacsen, displayed in Emacs 24 UI)
|
|
who read or edit by waving mouse at text
|
|
defaults
|
|
and keep possibly customized variables bound. Closes Trac #387.
|
|
|
|
|
|
|
|
|
|
Martin-Dorel)
|
|
convenience commands.
|
|
(i.e., automatic preview of next command)
|
|
|
|
with holes
mode (unfortunately).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
command elements.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
