diff options
| author |  Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-11-10 14:19:59 +0000 |
|---|---|---|
| committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-11-10 14:19:59 +0000 |
| commit | 22f538e19b8984689e360bcffe1780b77d5e88c9 (patch) | |
| tree | a229e189adf5ff942a56738286d1302f95482c79 | |
| parent | 544e0513a23f3806d44b6c39ffe382cf2acc9c5f (diff) | |
Refresh response buffer when goals buffer is refreshed.
| -rw-r--r-- | generic/proof-shell.el | 9 | ||||
| -rw-r--r-- | todo | 8 |
2 files changed, 11 insertions, 6 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 78e60a7c..0c3f7916 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -365,11 +365,14 @@ This is a list of tuples of the form (type . string). type is either (progn (aset out op c) (incf op))) (incf ip)) + + ;; Response buffer may be out of date. It may contain (error) + ;; messages relating to earlier proof states + (set-buffer proof-response-buffer) + (erase-buffer) + (set-buffer proof-pbp-buffer) (erase-buffer) - ;; Perhaps we ought to erase the proof-response-buffer at this - ;; point as well. It may contain an error message referring to - ;; an *earlier* state in the proof. (insert (substring out 0 op)) (proof-display-and-keep-buffer proof-pbp-buffer) @@ -389,9 +389,11 @@ X pbp code doesn't quite accord with the tech report; in particular it C fix Pbp implementation (10h) -B Equiv, Next,... aren't handled properly, because LEGO does not - refresh the proof state. Perhaps it would be easiest to get LEGO to - output more information in proof script mode (2h) +C Inoking an "Expand" command produces a new proof state. But this is + incorrectly displayed in the response buffer and not the goals + buffer because special annotations are missing. Presumably, one + ought to replace "Toplevel.Pr()" by "Toplevel.PR()" in the + definition of "Expand" (see file newtop.sml [Version 1.4]). (30min) B release new version of the LEGO proof engine (4h tms) |