diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-05-26 12:54:26 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-05-26 12:54:26 +0000 |
| commit | 2954ca8d555af6290aa7b94b09ccebe276b466be (patch) | |
| tree | ca81f3f1f15045b211ded6c037c5e3821a49dbe2 /generic/pg-goals.el | |
| parent | 51a8d16344647114cabfd481ac3cb2ddad7abfaa (diff) | |
Add proof-shell-strip-output-markup to handle pasting markedup texdt. Minor cleanups
Diffstat (limited to 'generic/pg-goals.el')
| -rw-r--r-- | generic/pg-goals.el | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/generic/pg-goals.el b/generic/pg-goals.el index 35ea669c..e3e53c5a 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.el @@ -101,13 +101,10 @@ Converts term substructure markup into mouse-highlighted extents." ;; Only display if string is non-empty. (unless (string-equal string "") + (setq buffer-read-only nil) (insert string) - - ;; Record a cleaned up version of output string - (setq proof-shell-last-output - (buffer-substring (point-min) (point-max))) - - (set-buffer-modified-p nil) ; nicety + (setq buffer-read-only t) + (set-buffer-modified-p nil) ;; Keep point at the start of the buffer. (proof-display-and-keep-buffer |