diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-11-12 14:20:16 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-11-12 14:20:16 +0000 |
| commit | c400fa8c8208f533c1928419614d11787c952053 (patch) | |
| tree | 1d20b954d47a5e91f49f015fc3ae21dfc523fa03 /lego | |
| parent | a4eeaebc3acf11643257a2c177c46a6f914be59e (diff) | |
Added setting for proof-goal-command-regexp
Diffstat (limited to 'lego')
| -rw-r--r-- | lego/lego.el | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/lego/lego.el b/lego/lego.el index 4dcaa46c..9c35572e 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -166,7 +166,7 @@ (define-derived-mode lego-mode proof-mode "lego" nil (lego-mode-config) - (easy-menu-change (list proof-mode-name) (car proof-help-menu) + (easy-menu-change (list proof-general-name) (car proof-help-menu) (append (cdr proof-help-menu) lego-help-menu-list))) (eval-and-compile @@ -375,6 +375,7 @@ Given is the first SPAN which needs to be undone." proof-stack-to-indent 'lego-stack-to-indent) (setq proof-save-command-regexp lego-save-command-regexp + proof-goal-command-regexp lego-goal-command-regexp proof-save-with-hole-regexp lego-save-with-hole-regexp proof-goal-with-hole-regexp lego-goal-with-hole-regexp proof-kill-goal-command lego-kill-goal-command |