diff options
| author | Thomas Kleymann | 1998-10-30 16:34:38 +0000 |
|---|---|---|
| committer | Thomas Kleymann | 1998-10-30 16:34:38 +0000 |
| commit | 00c337af2ea574baf01a26581b80aa1fd955e2f0 (patch) | |
| tree | bc522ddcd85ecae4f3db4fc007dc22b771d9591c /generic/proof-script.el | |
| parent | 4159c005b516ea482b6d0e5fc5e1d960348383c4 (diff) | |
implemented new buffer model. The goals buffer is now exclusively
reserved for goals.
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index fa09ede9..624a468e 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -272,10 +272,7 @@ to allow other files loaded by proof assistants to be marked read-only." (defun proof-warning (str) "Issue the warning STR." (proof-response-buffer-display str 'proof-warning-face) - (display-buffer proof-response-buffer) - (set-window-dedicated-p - (get-buffer-window proof-response-buffer) 'dedicated)) - + (proof-display-and-keep-buffer proof-response-buffer)) (defun proof-register-possibly-new-processed-file (file) "Register a possibly new FILE as having been processed by the prover." |