diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-04-07 09:42:02 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-04-07 09:42:02 +0000 |
| commit | 556e84c80c3bf9a49cf300572c1854ed2f05597b (patch) | |
| tree | 9b33fecebb34ea0bf93f0c6d4bc61503210ff319 /hol98 | |
| parent | 71f0f60954301df47a19e1b6778fb2348ab257a1 (diff) | |
Fixed up proof-shell-proof-completed mess nicely.
Diffstat (limited to 'hol98')
| -rw-r--r-- | hol98/hol98.el | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/hol98/hol98.el b/hol98/hol98.el index d2774915..98dce6d0 100644 --- a/hol98/hol98.el +++ b/hol98/hol98.el @@ -57,11 +57,7 @@ ;; FIXME: add optional help topic parameter to help command. ;; Have patch ready for PG 3.2, but PG 3.1 is strictly bug fix. proof-info-command "help \"hol\"" - ;; FIXME: Isabelle has introduced a mess here, and we need to fix it. - ;; See comments in proof-shell.el and proof-config.el and todo - proof-goals-display-qed-message t - proof-shell-proof-completed-regexp - "\\(.*Initial goal proved\\(.\\|\n\\)*\\)" + proof-shell-proof-completed-regexp "Initial goal proved" ;; FIXME: next one needs setting so that "urgent" messages are displayed ;; eagerly from HOL. ;; proof-shell-eager-annotation-start |