Repository navigation
Common toggles - #913
Merged
Merged
Common toggles#913
Conversation
The proof-deftoggle of proof-menu.el whose option is in proof-useropts.el go next to it, so that the toggles exist without the proof shell: proof-useropts.el is loaded by all backends. The toggle of proof-script-fly-past-comments, option of proof-config.el, and the per-prover ones stay in proof-menu.el. proof-useropts.el requires pg-pamacs (proof-deftoggle). No change otherwise. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Its lighter, proof-electric-terminator-enable and proof-electric-terminator-toggle move from pg-user.el to next to the option, so that other backends can use them. Without Proof General, the lighter shows nothing (proof-mode-for-script is unbound) and proof-double-hit-enable may be unbound: both are tested with boundp. The autoload of proof-electric-terminator-enable to pg-user is removed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…g width in common files. coq-show-proof-stepwise and its toggle move from coq.el to coq-goals.el, coq-Compile (make FILE.vo) to coq-compile-common.el, unchanged. New coq-auto-adapt-printing-width-toggle, next to the option in coq-goals.el. The PG menu is unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Toggle commands of the options without the proof shell
The PG menu is unchanged.