[nongnu] elpa/proof-general d6598d1ef1 1/2: Coq: make printing parentheses/notations flags accessible

[ELPA Syncer]

branch: elpa/proof-general
commit d6598d1ef1bbcd311639028d373e50fe345cacd8
Author: Hendrik Tews <hendrik@askra.de>
Commit: Hendrik Tews <hendrik@askra.de>

    Coq: make printing parentheses/notations flags accessible
    
    Add menu entry and Coq keymap binding available to set/unset the
    Printing Parentheses and Printing Notations flags.
---
 CHANGES           | 4 ++++
 coq/coq-abbrev.el | 4 ++++
 coq/coq.el        | 8 ++++++++
 3 files changed, 16 insertions(+)

diff --git a/CHANGES b/CHANGES
index f277190604..8e77207399 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 14658c51eb..3eefa60545 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -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]
diff --git a/coq/coq.el b/coq/coq.el
index 4eb4938106..2b83a1ddd4 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -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.")
@@ -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)))