diff options
| -rw-r--r-- | generic/proof-config.el | 12 | ||||
| -rw-r--r-- | generic/proof-script.el | 4 | ||||
| -rw-r--r-- | generic/proof-shell.el | 8 | ||||
| -rw-r--r-- | lego/lego.el | 4 |
4 files changed, 16 insertions, 12 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index bec16319..83b850bf 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -527,6 +527,18 @@ mere warning messages with this regexp)." :type 'regexp :group 'proof-shell) +(defcustom pbp-goal-command nil + "Command informing the prover that `pbp-button-action' has been + requested on a goal." + :type 'regexp + :group 'proof-shell) + +(defvar pbp-hyp-command nil + "Command informing the prover that `pbp-button-action' has been + requested on an assumption." + :type 'regexp + :group 'proof-shell) + (defcustom proof-shell-result-start "" "Regexp matching start of an output from the prover after pbp commands. In particular, after a `pbp-goal-command' or a `pbp-hyp-command'." diff --git a/generic/proof-script.el b/generic/proof-script.el index 4447f368..b423aed9 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1428,10 +1428,6 @@ finish setup which depends on specific proof assistant configuration." ;; calculate some strings and regexps for searching (setq proof-terminal-string (char-to-string proof-terminal-char)) - ;; FIXME: these are LEGO specific! - (setq pbp-goal-command (concat "Pbp %s" proof-terminal-string)) - (setq pbp-hyp-command (concat "PbpHyp %s" proof-terminal-string)) - ;; FIXME da: I'm not sure we ought to add spaces here, but if ;; we don't, there would be trouble overloading these settings ;; to also use as regexps for finding comments. diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 6e41ff6f..961466b7 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -227,14 +227,6 @@ Does nothing if proof assistant is already running." ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defvar pbp-goal-command nil - "Command informing the prover that `pbp-button-action' has been - requested on a goal.") - -(defvar pbp-hyp-command nil - "Command informing the prover that `pbp-button-action' has been - requested on an assumption.") - (defun pbp-button-action (event) (interactive "e") (mouse-set-point event) diff --git a/lego/lego.el b/lego/lego.el index 2ea0594e..3a6fe5d4 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -404,6 +404,10 @@ (lego-init-syntax-table) + ;; da: I've moved these out of proof-config-done in proof-script.el + (setq pbp-goal-command (concat "Pbp %s" proof-terminal-string)) + (setq pbp-hyp-command (concat "PbpHyp %s" proof-terminal-string)) + (proof-config-done) (define-key (current-local-map) [(control c) ?i] 'lego-intros) |