;;; coq-abbrev.el --- coq abbrev table and menus for ProofGeneral mode
;; Copyright (C) 1994 - 1998 LFCS Edinburgh. 
;; Authors: Healfdene Goguen, Pierre Courtieu
;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>

(require 'proof)
(require 'coq-syntax)

(defun holes-show-doc ()
  (interactive)
  (describe-variable 'holes-doc))

(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 t])
	  (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
(defun coq-install-abbrevs ()
  "install default abbrev table for coq if no other already is."
  (if (boundp 'coq-mode-abbrev-table)
      ;; da: this test will always fail.  Assume bound-->non-empty
      ;; (not (equal coq-mode-abbrev-table (make-abbrev-table))))
      (message "Coq abbrevs already exists, default not loaded")
    (define-abbrev-table 'coq-mode-abbrev-table
      (append coq-tactics-abbrev-table coq-tacticals-abbrev-table
	      coq-commands-abbrev-table coq-terms-abbrev-table))
    ;; if we use default coq abbrev, never ask to save it
    (setq save-abbrevs nil)
    (message "Coq default abbrevs loaded")
    ))

(unless noninteractive
  (coq-install-abbrevs))
;;;;;

;; The coq menu mainly built from tables

(defpgdefault menu-entries
  `(
    ["Toggle 3 windows mode" proof-three-window-toggle t]
     ""
    ["Print..." coq-Print t]
    ["Check..." coq-Check t]
    ["About..." coq-About t]
    ("OTHER QUERIES"
     ["Print Hint" coq-PrintHint t]
     ["Show ith goal..." coq-Show 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 t]
     ["Check..." coq-Check t]
     ["About..." coq-About t]
     ["Search..." coq-SearchConstant t]
     ["SearchRewrite..." coq-SearchRewrite t]
     ["SearchAbout..." coq-SearchAbout 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]
     )
     ""
    ("INSERT"
     ""
     ["tactic (interactive)" coq-insert-tactic t]
     ,coq-tactics-menu
     ["tactical (interactive)" coq-insert-tactical t]
     ,coq-tacticals-menu
     ""
     ["command (interactive)" coq-insert-command t]
     ,coq-commands-menu
     ""
     ["term (interactive)" coq-insert-term t]
     ,coq-terms-menu
     ""
     ["Module/Section (smart)" coq-insert-section-or-module t]
     ["Require (smart)" coq-insert-requires t])
    ;; da: I added Show sub menu, not sure if it's helpful, but why not.
    ;; FIXME: submenus should be split off here.  Also, these commands
    ;; should only be available when a proof is open.
    ;; pc: I added things in the show menu and called it QUERIES

    ""
    ("HOLES"
     ;; da: I tidied this menu a bit.  I personally think this "trick"
     ;; of inserting strings to add documentation looks like a real
     ;; mess in menus ... I've removed it for the three below since
     ;; the docs below appear in popup in messages anyway.
     ;;
     ;; "Make a hole active   click on it"
     ;; "Disable a hole   click on it (button 2)"
     ;; "Destroy a hole   click on it (button 3)"
     ["Make hole at point"  holes-set-make-active-hole t]
     ["Make selection a hole"  holes-set-make-active-hole t]
     ["Replace active hole by selection"  holes-replace-update-active-hole t]
     ["Jump to active hole"  holes-set-point-next-hole-destroy t]
     ["Forget all holes in buffer"  holes-clear-all-buffer-holes t]
     ["Tell me about holes?" holes-show-doc t]
     ;; look a bit better at the bottom
     "Make hole with mouse: C-M-select"
     "Replace hole with mouse: C-M-Shift select";; da: does this one work??
     )

    ;; da: I also added abbrev submenu.  Surprising Emacs doesn't have one?
    ("ABBREVS"
     ["Expand at point" expand-abbrev t]
     ["Unexpand last" unexpand-abbrev t]
     ["List abbrevs" list-abbrevs t]
     ["Edit abbrevs" edit-abbrevs t];; da: is it OK to add edit?
     ["Abbrev mode" abbrev-mode
      :style toggle
      :selected (and (boundp 'abbrev-mode) abbrev-mode)])
    ;; With all these submenus you have to wonder if these things belong
    ;; on the main menu.  Are they the most often used?
    ""
    ("COQ PROG (ARGS)"
     ["Set coq prog *persistently*" coq-ask-insert-coq-prog-name t]
     ["help on setting persistently" coq-local-vars-list-show-doc t]
     ["Compile" coq-Compile t])
    ))

;; da: Moved this from the main menu to the Help submenu.
;; It also appears under Holes, anyway.
(defpgdefault help-menu-entries
  '(["Tell me about holes?" holes-show-doc t]
    ["help on setting prog name persistently for a file" coq-local-vars-list-show-doc t]))


(provide 'coq-abbrev)