Skip to content

Commit

Permalink
Coq: make printing parentheses/notations flags accessible
Browse files Browse the repository at this point in the history
Add menu entry and Coq keymap binding available to set/unset the
Printing Parentheses and Printing Notations flags.
  • Loading branch information
hendriktews committed Sep 12, 2024
1 parent 5e14b97 commit d6598d1
Show file tree
Hide file tree
Showing 3 changed files with 16 additions and 0 deletions.
4 changes: 4 additions & 0 deletions CHANGES
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
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
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

0 comments on commit d6598d1

Please sign in to comment.