Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Coq: make printing parentheses flag accessible #785

Merged
merged 1 commit into from
Sep 12, 2024
Merged

Coq: make printing parentheses flag accessible #785

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions CHANGES
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,10 @@ the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG
*** New command `proof-check-annotate' to annotate all failing proofs
with FAIL comments. Useful in the development process as described
above to ensure all currently failing proofs are marked as such.
*** flag Printing Parentheses and Printing Notations can be set/unset
via menu and Coq keymap (C-c C-a C-9 and C-c C-a C-0 for
Parentheses (optimized for British and American keyboards); C-c
C-a n and C-c C-a N for Notations).
*** New options coq-compile-extra-coqc-arguments and
coq-compile-extra-coqdep-arguments to configure additional
command line arguments to calls of, respetively, coqc and coqdep
Expand Down
4 changes: 4 additions & 0 deletions coq/coq-abbrev.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -335,6 +335,10 @@
["Unset Printing All" coq-unset-printing-all t]
["Set Printing Implicit" coq-set-printing-implicit t]
["Unset Printing Implicit" coq-unset-printing-implicit t]
["Set Printing Parentheses" coq-set-printing-parentheses t]
["Unset Printing Parentheses" coq-unset-printing-parentheses t]
["Set Printing Notations" coq-set-printing-notations t]
["Unset Printing Notations" coq-unset-printing-notations t]
["Set Printing Coercions" coq-set-printing-coercions t]
["Unset Printing Coercions" coq-unset-printing-coercions t]
["Set Printing Compact Contexts" coq-set-printing-implicit t]
Expand Down
8 changes: 8 additions & 0 deletions coq/coq.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1771,6 +1771,10 @@ See `coq-fold-hyp'."
(proof-definvisible coq-unset-printing-implicit "Unset Printing Implicit.")
(proof-definvisible coq-set-printing-all "Set Printing All.")
(proof-definvisible coq-unset-printing-all "Unset Printing All.")
(proof-definvisible coq-set-printing-parentheses "Set Printing Parentheses.")
(proof-definvisible coq-unset-printing-parentheses "Unset Printing Parentheses.")
(proof-definvisible coq-set-printing-notations "Set Printing Notations.")
(proof-definvisible coq-unset-printing-notations "Unset Printing Notations.")
(proof-definvisible coq-set-printing-synth "Set Printing Synth.")
(proof-definvisible coq-unset-printing-synth "Unset Printing Synth.")
(proof-definvisible coq-set-printing-coercions "Set Printing Coercions.")
Expand Down Expand Up @@ -2861,6 +2865,10 @@ Completion is on a quasi-exhaustive list of Coq tacticals."
(define-key coq-keymap [(control ?l)] #'coq-LocateConstant)
(define-key coq-keymap [(control ?n)] #'coq-LocateNotation)
(define-key coq-keymap [(control ?w)] #'coq-ask-adapt-printing-width-and-show)
(define-key coq-keymap [(control ?9)] #'coq-set-printing-parentheses)
(define-key coq-keymap [(control ?0)] #'coq-unset-printing-parentheses)
(define-key coq-keymap [(?N)] #'coq-set-printing-notations)
(define-key coq-keymap [(?n)] #'coq-unset-printing-notations)

;(proof-eval-when-ready-for-assistant
; (define-key ??? [(control c) (control a)] (proof-ass keymap)))
Expand Down
Loading