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 | |
| parent | 1e478c22cda609e91c21a17cf14fa86c05fef42c (diff) | |
Remove barely useful proof-shell-abort-goal-regexp (only served to sanitize LEGO messages)
| -rw-r--r-- | generic/proof-config.el | 5 | ||||
| -rw-r--r-- | isar/isar.el | 1 | ||||
| -rw-r--r-- | lego/lego.el | 6 | ||||
| -rw-r--r-- | plastic/plastic.el | 5 |
4 files changed, 0 insertions, 17 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 83c0c4f7..a4b9bb0f 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1091,11 +1091,6 @@ in ordinary output, which should appear in this regexp." :type 'regexp :group 'proof-shell) -(defcustom proof-shell-abort-goal-regexp nil - "Regexp matching output from an aborted proof." - :type 'regexp - :group 'proof-shell) - (defcustom proof-shell-error-regexp nil "Regexp matching an error report from the proof assistant. diff --git a/isar/isar.el b/isar/isar.el index a1ca86a1..19abfedc 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -183,7 +183,6 @@ See -k option for Isabelle interface script." proof-shell-interrupt-regexp "\^AM\\*\\*\\* Interrupt" proof-shell-error-regexp "\^AM\\*\\*\\*" proof-shell-proof-completed-regexp nil ; n.a. - proof-shell-abort-goal-regexp nil ; n.a. pg-next-error-regexp "\\((line \\([0-9]+\\) of \"[^\"]+\")\\)" pg-next-error-filename-regexp "\\((line [0-9]+ of \"\\([^\"]+\\)\")\\)" 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 diff --git a/plastic/plastic.el b/plastic/plastic.el index 5a7a7f03..2fceda64 100644 --- a/plastic/plastic.el +++ b/plastic/plastic.el @@ -125,10 +125,6 @@ (concat plastic-lit-string " &S ECHO no cd ;\n") "*Command of the inferior process to change the directory.") -(defvar plastic-shell-abort-goal-regexp "KillRef: ok, not in proof state" - "*Regular expression indicating that the proof of the current goal - has been abandoned.") - (defvar plastic-shell-proof-completed-regexp "\\*\\*\\* QED \\*\\*\\*" "*Regular expression indicating that the proof has been completed.") @@ -451,7 +447,6 @@ For Plastic, we assume that module identifiers coincide with file names." (defun plastic-shell-mode-config () (setq proof-shell-cd-cmd plastic-shell-cd - proof-shell-abort-goal-regexp plastic-shell-abort-goal-regexp proof-shell-proof-completed-regexp plastic-shell-proof-completed-regexp proof-shell-error-regexp plastic-error-regexp proof-shell-interrupt-regexp plastic-interrupt-regexp |