From 9e875cc8caad464331a0628a037e3d3e30aa4449 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 15 Jan 2008 13:01:45 +0000 Subject: New files. --- generic/pg-custom.el | 180 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 180 insertions(+) create mode 100644 generic/pg-custom.el (limited to 'generic/pg-custom.el') diff --git a/generic/pg-custom.el b/generic/pg-custom.el new file mode 100644 index 00000000..f977ae97 --- /dev/null +++ b/generic/pg-custom.el @@ -0,0 +1,180 @@ +;;; pg-custom.el --- Proof General per-prover settings +;; +;; Copyright (C) 2008 LFCS Edinburgh. +;; Author: David Aspinall and others +;; License: GPL (GNU GENERAL PUBLIC LICENSE) +;; +;;; Commentary: +;; +;; Prover specific settings +;; +;; The settings defined here automatically use the current proof +;; assistant symbol as a prefix, i.e. isa-favourites, coq-favourites, +;; or whatever will be defined on evaluation. +;; +;; This file is loaded only by mode stubs defined in `proof-site.el', +;; immediately after `proof-assistant' and similar settings have been +;; configured. +;; +;; WARNING: loading this file without these variables being set will +;; give errors, because defpgcustom calls are expanded to top-level +;; forms that refer to `proof-assistant', which is only properly set +;; when the mode for a proof assistant is started (see mode stub). +;; + +;;; Code: + +(require 'proof-utils) ; defpgcustom +(require 'proof-config) ; for proof-toolbar-entries-default + +(defpgcustom x-symbol-enable nil + "*Whether to use x-symbol in Proof General for this assistant. +If you activate this variable, whether or not you really get x-symbol +support depends on whether your proof assistant supports it and +whether X-Symbol is installed in your Emacs." + :type 'boolean + :set 'proof-set-value + :group 'proof-user-options) + +(defpgcustom x-symbol-language proof-assistant-symbol + "Setting for x-symbol-language for the current proof assistant. +It defaults to proof-assistant-symbol, which makes X Symbol +look for files named x-symbol-.el.") + +(defpgcustom maths-menu-enable nil + "*Non-nil for Unicode maths menu in Proof General for this assistant." + :type 'boolean + :set 'proof-set-value + :group 'proof-user-options) + +(defpgcustom mmm-enable nil + "*Whether to use MMM Mode in Proof General for this assistant. +MMM Mode allows multiple modes to be used in the same buffer. +If you activate this variable, whether or not you really get MMM +support depends on whether your proof assistant supports it." + :type 'boolean + :set 'proof-set-value + :group 'proof-user-options) + +(defpgcustom script-indent t + "*If non-nil, enable indentation code for proof scripts." + :type 'boolean + :group 'proof-user-options) + +(defconst proof-toolbar-entries-default + `((state "Display Proof State" "Display the current proof state" t + proof-showproof-command) + (context "Display Context" "Display the current context" t + proof-context-command) +;; PG 3.7: disable goal & qed, they're not so useful (& save-command never enabled). +;; (goal "Start a New Proof" "Start a new proof" t +;; proof-goal-command) + (retract "Retract Buffer" "Retract (undo) whole buffer" t) + (undo "Undo Step" "Undo the previous proof command" t) + (delete "Delete Step" nil t) + (next "Next Step" "Process the next proof command" t) + (use "Use Buffer" "Process whole buffer" t) + (goto "Goto Point" "Process or undo to the cursor position" t) +;; (qed "Finish Proof" "Close/save proved theorem" t +;; proof-save-command) + (lockedend "Goto Locked End" nil t) + (find "Find Theorems" "Find theorems" t proof-find-theorems-command) + (command "Issue Command" "Issue a non-scripting command" t) + (interrupt "Interrupt Prover" "Interrupt the proof assistant" t) + (restart "Restart Scripting" "Restart scripting (clear all locked regions)" t) + (visibility "Toggle Visibility" nil t) +; PG 3.6: remove Info item from toolbar; it's not very useful and under PA->Help anyway +; (info nil "Show online proof assistant information" t +; proof-info-command) +; PG 3.7: use Info icon for info + (info nil "Proof General manual" t)) +"Example value for proof-toolbar-entries. Also used to define scripting menu. +This gives a bare toolbar that works for any prover, providing the +appropriate configuration variables are set. +To add/remove prover specific buttons, adjust the `-toolbar-entries' +variable, and follow the pattern in `proof-toolbar.el' for +defining functions, images.") + +(defpgcustom toolbar-entries proof-toolbar-entries-default + "List of entries for Proof General toolbar and Scripting menu. +Format of each entry is (TOKEN MENUNAME TOOLTIP DYNAMIC-ENABLER-P ENABLE). + +For each TOKEN, we expect an icon with base filename TOKEN, +a function proof-toolbar-, and (optionally) a dynamic enabler +proof-toolbar--enable-p. + +If ENABLEP is absent, item is enabled; if ENABLEP is present, item +is only added to menubar and toolbar if ENABLEP is non-null. + +If MENUNAME is nil, item will not appear on the scripting menu. + +If TOOLTIP is nil, item will not appear on the toolbar. + +The default value is `proof-toolbar-entries-default' which contains +the standard Proof General buttons.") + +(defpgcustom prog-args nil + "Arguments to be passed to `proof-prog-name' to run the proof assistant. +If non-nil, will be treated as a list of arguments for`proof-prog-name'. +Otherwise `proof-prog-name' will be split on spaces to form arguments. + +Remark: Arguments are interpreted strictly: each one must contain only one +word, with no space (unless it is the same word). For example if the +arguments are -x foo -y bar, then the list should be '(\"-x\" \"foo\" +\"-y\" \"bar\"), notice that '(\"-x foo\" \"-y bar\") is *wrong*" + + :type '(list string) + :group 'proof-shell) + +(defpgcustom prog-env nil + "Modifications to `process-environment' made before running `proof-prog-name'. +Each element should be a string of the form ENVVARNAME=VALUE. They will be +added to the environment before launching the prover (but not pervasively). +For example for coq on Windows you might need something like: +(setq coq-prog-env '(\"HOME=C:\\Program Files\\Coq\\\"))" + :type '(list string) + :group 'proof-shell) + +(defpgcustom favourites nil + "*Favourite commands for this proof assistant. +A list of lists of the form (COMMAND INSCRIPT MENUNAME KEY), +arguments for `proof-add-favourite', which see.") + +(defpgcustom menu-entries nil + "Extra entries for proof assistant specific menu. +A list of menu items [NAME CALLBACK ENABLER ...]. See the documentation +of `easy-menu-define' for more details." + :type 'sexp + :group 'prover-config) + +(defpgcustom help-menu-entries nil + "Extra entries for help submenu for proof assistant specific help menu. +A list of menu items [NAME CALLBACK ENABLER ...]. See the documentation +of `easy-menu-define' for more details." + :type 'sexp + :group 'prover-config) + +(defpgcustom keymap (make-keymap (concat proof-assistant " keymap")) + "Proof assistant specific keymap, used under prefix C-c a." + :type 'sexp + :group 'prover-config) + +(defpgcustom completion-table nil + "List of identifiers to use for completion for this proof assistant. +Completion is activated with \\[complete]. + +If this table is empty or needs adjusting, please make changes using +`customize-variable' and post suggestions at +http://proofgeneral.inf.ed.ac.uk/trac" + :type '(list string) + :group 'prover-config) + +;; TODO: not used yet. +(defpgcustom tags-program nil + "Program to run to generate TAGS table for proof assistant." + :type 'file + :group 'prover-config) + +(provide 'pg-custom) + +;;; pg-custom.el ends here -- cgit v1.2.3