Repository navigation
Common menus - #914
Merged
Merged
Common menus#914
Conversation
…onstants. Like coq-compile-menu, coq-hyps-menu and coq-insert-menu: the entries written in coq-abbrev.el move next to their commands, so that other backends can use them. coq-queries.el: coq-queries-menu-entries (the main queries and Store Goal/Response, at the top level of the PG menu), coq-other-queries-menu and coq-options-menu. coq-templates.el: coq-abbrevs-menu. coq-project.el: coq-project-menu-entries. The PG menu is unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The command common to all backends, which calls coq-ask-printing-width-function: for Proof General, the same coq-ask-adapt-printing-width-and-show as before. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
coq-ask-adapt-printing-width-and-show (C-c C-a C-w, menu OPTIONS -> Set Printing Width) did nothing when coq-auto-adapt-printing-width was nil: coq-adapt-printing-width tested it. New optional argument FORCE of coq-adapt-printing-width, given by the command asking the width. 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.
Coq: the menus of the queries, options, abbrevs and project file shared by all backends
These menus become constants, like coq-compile-menu, coq-hyps-menu and coq-insert-menu, so that other backends can use them:
"Set Printing Width" now goes through the common command coq-ask-printing-width, which does the same as before in PG. Otherwise the PG menu is unchanged (checked by comparing it with master's).
Test: every command of the shared menus is defined without Proof General. Also a CHANGES entry.