Merge pull request ProofGeneral#785 from hendriktews/paren

Coq: make printing parentheses flag accessible

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

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]

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)))