;;; coq-abbrev.el --- coq abbrev table and menus for ProofGeneral mode -*- lexical-binding:t -*- ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh ;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews ;; Portions © Copyright 2015-2017 Clément Pit-Claudel ;; Authors: Healfdene Goguen, Pierre Courtieu ;; Maintainer: Pierre Courtieu ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;;; Commentary: ;; ;;; Code: (require 'proof) (require 'coq-syntax) (defun holes-show-doc () (interactive) (describe-function 'holes-mode)) (defun coq-local-vars-list-show-doc () (interactive) (describe-variable 'coq-local-vars-doc)) (defconst coq-tactics-menu (append '("Tactics (menu)" ["Intros (smart)" coq-insert-intros :help "Insert \"intros h1 .. hn.\" where hi are the default names given by Coq."]) (coq-build-menu-from-db (append coq-tactics-db coq-solve-tactics-db)))) (defconst coq-tactics-abbrev-table (coq-build-abbrev-table-from-db (append coq-tactics-db coq-solve-tactics-db))) (defconst coq-tacticals-menu (append '("Tacticals (menu)") (coq-build-menu-from-db coq-tacticals-db))) (defconst coq-tacticals-abbrev-table (coq-build-abbrev-table-from-db coq-tacticals-db)) (defconst coq-commands-menu (append '("Command (menu)" ;["Module/Section (smart)" coq-insert-section-or-module t] ;["Require (smart)" coq-insert-requires t] ) (coq-build-menu-from-db coq-commands-db))) (defconst coq-commands-abbrev-table (coq-build-abbrev-table-from-db coq-commands-db)) (defconst coq-terms-menu (append '("Term (menu)" ["Match (smart)" coq-insert-match t]) (coq-build-menu-from-db coq-terms-db))) (defconst coq-terms-abbrev-table (coq-build-abbrev-table-from-db coq-terms-db)) ;;; The abbrev table built from keywords tables ;#s and @{..} are replaced by holes by holes-abbrev-complete (define-abbrev-table 'coq-mode-abbrev-table (append coq-tactics-abbrev-table coq-tacticals-abbrev-table coq-commands-abbrev-table coq-terms-abbrev-table) "Abbrev table for Coq.") ;; The coq menu partly built from tables ;; Common part (script, response and goals buffers) (defconst coq-menu-common-entries `( ["Toggle 3 Windows Mode" proof-three-window-toggle :style toggle :selected proof-three-window-enable :help "Toggles the use of separate windows or frames for Coq responses and goals." ] ("3 Windows mode layout" ["smart" (progn (customize-set-variable 'proof-three-window-mode-policy 'smart) (proof-layout-windows)) :style radio :selected (eq proof-three-window-mode-policy 'smart) :help "Adapt to frame width (C-c C-l to refresh)"] ["hybrid" (progn (customize-set-variable 'proof-three-window-mode-policy 'hybrid) (proof-layout-windows)) :style radio :selected (eq proof-three-window-mode-policy 'hybrid) :help "two column mode"] ["horizontal" (progn (customize-set-variable 'proof-three-window-mode-policy 'horizontal) (proof-layout-windows)) :style radio :selected (eq proof-three-window-mode-policy 'horizontal) :help "Three column mode"] ["vertical" (progn (customize-set-variable 'proof-three-window-mode-policy 'vertical) (proof-layout-windows)) :style radio :selected (eq proof-three-window-mode-policy 'vertical) :help "One column mode"]) ["Refresh Windows Layout" proof-layout-windows t] ["Toggle tooltips" proof-output-tooltips-toggle :style toggle :selected proof-output-tooltips :help "Toggles Tooltips (popup when hovering commands).\nSet `proof-output-tooltips' to nil to disable it by default."] ["Electric Terminator" proof-electric-terminator-toggle :style toggle :selected proof-electric-terminator-enable :help "Automatically send commands when terminator typed"] ["Double Hit Electric Terminator" coq-double-hit-toggle :style toggle :selected coq-double-hit-enable :help "Automatically send commands when terminator typed twiced quickly."] ("Auto Compilation" ["Compile Before Require" coq-compile-before-require-toggle :style toggle :selected coq-compile-before-require :help "Check dependencies of required modules and compile on the fly."] ["Parallel background compilation" coq-compile-parallel-in-background-toggle :style toggle :selected coq-compile-parallel-in-background :active coq-compile-before-require :help ,(concat "Compile parallel in background or " "sequentially with blocking ProofGeneral.")] ["Keep going" coq-compile-keep-going-toggle :style toggle :selected coq-compile-keep-going :active (and coq-compile-before-require coq-compile-parallel-in-background) :help ,(concat "Continue background compilation after " "the first error as far as possible")] ("Quick compilation" ["no quick" (customize-set-variable 'coq-compile-quick 'no-quick) :style radio :selected (eq coq-compile-quick 'no-quick) :active (and coq-compile-before-require coq-compile-parallel-in-background) :help "Compile without -quick but accept existion .vio's"] ["quick no vio2vo" (customize-set-variable 'coq-compile-quick 'quick-no-vio2vo) :style radio :selected (eq coq-compile-quick 'quick-no-vio2vo) :active (and coq-compile-before-require coq-compile-parallel-in-background) :help "Compile with -quick, accept existing .vo's, don't run vio2vo"] ["quick and vio2vo" (customize-set-variable 'coq-compile-quick 'quick-and-vio2vo) :style radio :selected (eq coq-compile-quick 'quick-and-vio2vo) :active (and coq-compile-before-require coq-compile-parallel-in-background) :help "Compile with -quick, accept existing .vo's, run vio2vo later"] ["ensure vo" (customize-set-variable 'coq-compile-quick 'ensure-vo) :style radio :selected (eq coq-compile-quick 'ensure-vo) :active (and coq-compile-before-require coq-compile-parallel-in-background) :help "Ensure only vo's are used for consistency"] ) ("Auto Save" ["Query coq buffers" (customize-set-variable 'coq-compile-auto-save 'ask-coq) :style radio :selected (eq coq-compile-auto-save 'ask-coq) :active coq-compile-before-require :help "Ask for each coq-mode buffer, except the current buffer"] ["Query all buffers" (customize-set-variable 'coq-compile-auto-save 'ask-all) :style radio :selected (eq coq-compile-auto-save 'ask-all) :active coq-compile-before-require :help "Ask for all buffers"] ["Autosave coq buffers" (customize-set-variable 'coq-compile-auto-save 'save-coq) :style radio :selected (eq coq-compile-auto-save 'save-coq) :active coq-compile-before-require :help "Save all Coq buffers without confirmation, except the current one"] ["Autosave all buffers" (customize-set-variable 'coq-compile-auto-save 'save-all) :style radio :selected (eq coq-compile-auto-save 'save-all) :active coq-compile-before-require :help "Save all buffers without confirmation"] ) ["Lock Ancesotors" coq-lock-ancestors-toggle :style toggle :selected coq-lock-ancestors :active coq-compile-before-require :help "Lock files of imported modules"] ["Confirm External Compilation" coq-confirm-external-compilation-toggle :style toggle :selected coq-confirm-external-compilation :active (and coq-compile-before-require (not (equal coq-compile-command ""))) :help "Confirm external compilation command, see `coq-compile-command'."] ["Abort Background Compilation" coq-par-emergency-cleanup :active (and coq-compile-before-require coq-compile-parallel-in-background) :help "Abort background compilation and kill all compilation processes."]) "" ["Print..." coq-Print :help "With prefix arg (C-u): Set Printing All first"] ["Check..." coq-Check :help "With prefix arg (C-u): Set Printing All first"] ["About..." coq-About :help "With prefix arg (C-u): Set Printing All first"] ["Other..." coq-query] [ "Store Response" proof-store-response-win :help "Stores the content of response buffer in a dedicated buffer"] [ "Store Goal" proof-store-goals-win :help "Stores the content of goals buffer in a dedicated buffer"] ("OTHER QUERIES" ["Print Hint" coq-PrintHint t] ["Show ith Goal..." coq-Show t] ["Show ith Goal... (show implicits)" coq-Show-with-implicits t] ["Show ith Goal... (show all)" coq-Show-with-all t] ["Show Tree" coq-show-tree t] ["Show Proof" coq-show-proof t] ["Show Conjectures" coq-show-conjectures t];; maybe not so useful with editing in PG? "" ["Print..." coq-Print :help "With prefix arg (C-u): Set Printing All first"] ["Print... (show implicits)" coq-Print-with-implicits t] ["Print... (show all)" coq-Print-with-all t] ["Check..." coq-Check :help "With prefix arg (C-u): Set Printing All first"] ["Check (show implicits)..." coq-Check-show-implicits t] ["Check (show all)..." coq-Check-show-all t] ["About..." coq-About :help "With prefix arg (C-u): Set Printing All first"] ["About...(show implicits)" coq-About-with-implicits t] ["About...(show all)" coq-About-with-all t] ["Search..." coq-SearchConstant t] ["SearchRewrite..." coq-SearchRewrite t] ["SearchAbout (hiding principles)..." coq-SearchAbout t] ["SearchAbout..." coq-SearchAbout-all t] ["SearchPattern..." coq-SearchIsos t] ["Locate constant..." coq-LocateConstant t] ["Locate Library..." coq-LocateLibrary t] ["Pwd" coq-Pwd t] ["Inspect..." coq-Inspect t] ["Print Section..." coq-PrintSection t] "" ["Locate notation..." coq-LocateNotation t] ["Print Implicit..." coq-Print t] ["Print Scope/Visibility..." coq-PrintScope t]) ("OPTIONS" ["Set Printing All" coq-set-printing-all t] ["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 Coercions" coq-set-printing-coercions t] ["Unset Printing Coercions" coq-unset-printing-coercions t] ["Set Printing Compact Contexts" coq-set-printing-implicit t] ["Unset Printing Compact Contexts" coq-unset-printing-implicit t] ["Set Printing Synth" coq-set-printing-synth t] ["Unset Printing Synth" coq-unset-printing-synth t] ["Set Printing Universes" coq-set-printing-universes t] ["Unset Printing Universes" coq-unset-printing-universes t] ["Set Printing Unfocused" coq-set-printing-unfocused t] ["Unset Printing Unfocused" coq-unset-printing-unfocused t] ["Set Printing Wildcards" coq-set-printing-wildcards t] ["Unset Printing Wildcards" coq-unset-printing-wildcards t] ["Set Printing Width" coq-ask-adapt-printing-width-and-show t]))) (setq-default coq-menu-entries (append coq-menu-common-entries `( "" ("INSERT" ["Intros (smart)" coq-insert-intros :help "Insert \"intros h1 .. hn.\" where hi are the default names given by Coq."] "" ["Tactic (interactive)" coq-insert-tactic t] ["Tactical (interactive)" coq-insert-tactical t] ["Command (interactive)" coq-insert-command t] ["Term (interactive)" coq-insert-term t] "" ,coq-tactics-menu ,coq-tacticals-menu ,coq-commands-menu ,coq-terms-menu "" ["Module/Section (smart)" coq-insert-section-or-module t] ["Require (smart)" coq-insert-requires t]) "" ("ABBREVS" ["Expand At Point" expand-abbrev t] ["Unexpand Last" unexpand-abbrev t] ["List Abbrevs" list-abbrevs t] ["Edit Abbrevs" edit-abbrevs t] ["Abbrev Mode" abbrev-mode :style toggle :selected (and (boundp 'abbrev-mode) abbrev-mode)]) "" ("COQ PROG (ARGS)" ["Use project file" coq-toggle-use-project-file :style toggle :selected (and (boundp 'coq-use-project-file) coq-use-project-file) ] ["Set Coq Prog *persistently*" coq-ask-insert-coq-prog-name t] ["help" coq-local-vars-list-show-doc t] ["Compile" coq-Compile t])))) (setq-default coq-help-menu-entries '(["help on setting prog name persistently for a file" coq-local-vars-list-show-doc t])) (setq-default coq-other-buffers-menu-entries coq-menu-common-entries) (provide 'coq-abbrev) ;;; coq-abbrev.el ends here