diff options
| author | David Aspinall | 1999-09-28 14:44:15 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-09-28 14:44:15 +0000 |
| commit | dae4fc095488a023cfacecb089eb6ff7d004a7c5 (patch) | |
| tree | b8fb5065012077c31ab8b3e405ed413d23d77884 /generic/proof-script.el | |
| parent | a0c18b6daff19a09aca6dd4146b24dca27ce5c2e (diff) | |
Made Scripting menu entry item on menubar.
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 72fafb34..a2858768 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1821,14 +1821,18 @@ finish setup which depends on specific proof assistant configuration." (if proof-script-indent (setq indent-line-function 'proof-indent-line)) - ;; Toolbar - ;; (NB: autloads proof-toolbar, which extends proof-menu variable) + ;; Toolbar and scripting menu + ;; NB: autloads proof-toolbar, which defines proof-toolbar-scripting-menu. (proof-toolbar-setup) + (easy-menu-define proof-mode-script-menu + proof-mode-map + "Scripting menu of Proof General" + proof-toolbar-scripting-menu) ;; Menu (easy-menu-define proof-mode-menu proof-mode-map - "Menu used in Proof General scripting mode." + "Proof General menu" (cons proof-general-name (append (cdr proof-menu) @@ -1843,7 +1847,12 @@ finish setup which depends on specific proof assistant configuration." nil) ;; end UGLY COMPATIBILTY HACK ))) + + ;; Put the ProofGeneral menu first on the menubar, then Scripting menu + ;; (makes Scripting menu more obvious) (easy-menu-add proof-mode-menu proof-mode-map) + (easy-menu-add proof-mode-script-menu proof-mode-map) + ;; For fontlock |