diff options
| -rw-r--r-- | generic/proof-config.el | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 400ec3e3..53e0faff 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1415,6 +1415,18 @@ See also proof-{shell,resp,goals}-font-lock-keywords." :group 'proof-script) +;; +;; Proof script context menu customization +;; +(defcustom proof-script-span-context-menu-extensions nil + "Extensions for the in-span context sensitive menu. +This should be a function which accepts three arguments: SPAN IDIOM NAME. +See pg-user.el: pg-create-in-span-context-menu for more hints." + :type 'function + :group 'proof-script) + + + @@ -1935,6 +1947,16 @@ The matching string will be parsed as XML and then processed by :type '(choice nil regexp) :group 'proof-shell) +;; FIXME FIXME: this next one not yet used. It's hard to interleave +;; commands with the ordinary queue anyway: the prover should +;; automatically output this information if it is enabled. +(defcustom proof-shell-query-dependencies-cmd nil + "Command to query the prover for dependencies of given theorem name. +%s is replaced by the name of the theorem. This command will be +sent when a proof is completed." + :type 'string + :group 'proof-shell) + (defcustom proof-shell-theorem-dependency-list-regexp nil "Regexp matching output telling Proof General what the dependencies are. This is so that the dependent theorems can be highlighted somehow. |