Save more space/fix display anomolay by leaving point at end of non-whitespace

1 files changed, 12 insertions, 5 deletions

diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index d76c4f1f..4b88e69f 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -505,13 +505,20 @@ Ensure that point is visible in window."
 		 ;; otherwise the window will adopt to the smallest
 		 ;; sized output for good.
 		 (proof-resize-window-tofit))
-	     ;; For various reasons, point may get moved
-	     ;; around in response buffer.
+	     ;; For various reasons, point may get moved around in
+	     ;; response buffer.  Attempt to normalise its position.
 	     (goto-char (or pos (point-max)))
-	     (if pos (beginning-of-line))
+	     (if pos 
+		 (beginning-of-line)
+	       (skip-chars-backward "\n\t "))
 	     ;; Ensure point visible
-	     (or (pos-visible-in-window-p (point) window)
-		 (recenter -1)))))))
+	     (or 
+	      ;; FIXME: test proof-shrink-windows-tofit here as a
+	      ;; hack to avoid odd/bad behaviour of shrinking
+	      ;; moving window contents beyond start of display
+	      proof-shrink-windows-tofit
+	      (pos-visible-in-window-p (point) window)
+	      (recenter -1)))))))
 
 (defun proof-clean-buffer (buffer)
   "Erase buffer and hide from display if proof-delete-empty-windows set.