diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-09-08 21:02:28 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-09-08 21:02:28 +0000 |
| commit | aff2ea4bbb63aff1a85b759e5541e3b7683d9776 (patch) | |
| tree | c470def269b803c9421b31700eb3683f556ffdf8 /lego | |
| parent | 1e478c22cda609e91c21a17cf14fa86c05fef42c (diff) | |
Remove barely useful proof-shell-abort-goal-regexp (only served to sanitize LEGO messages)
Diffstat (limited to 'lego')
| -rw-r--r-- | lego/lego.el | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/lego/lego.el b/lego/lego.el index 73552f20..be48be41 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -104,11 +104,6 @@ Activates extended printing routines required for Proof General.") (defvar lego-shell-cd "Cd \"%s\";" "*Command of the inferior process to change the directory.") -(defvar lego-shell-abort-goal-regexp - "KillRef: ok, not in proof state\\|Forget forced KillRef" - "*Regular expression indicating that the proof of the current goal - has been abandoned.") - (defvar lego-shell-proof-completed-regexp "\\*\\*\\* QED \\*\\*\\*" "*Regular expression indicating that the proof has been completed.") @@ -380,7 +375,6 @@ For LEGO, we assume that module identifiers coincide with file names." (defun lego-shell-mode-config () (setq proof-shell-cd-cmd lego-shell-cd - proof-shell-abort-goal-regexp lego-shell-abort-goal-regexp proof-shell-proof-completed-regexp lego-shell-proof-completed-regexp proof-shell-error-regexp lego-error-regexp proof-shell-interrupt-regexp lego-interrupt-regexp |