Sledgehammer output broken

[David Aspinall]

Output appears in *isabelle* buffer but not response buffer.

Waiting for further information.

[Makarius]

This problem is caused by the proof-shell-urgent-message-scanner marker being moved past the comint output. This unexpected behaviour seems to be a side effect of the removal of annotations from the shell buffer, see proof-shell.el revision 8.32.

The following modification of pg-remove-specials (which messes up regular term output!) is able to recover asynchronous urgent messages:

diff -r9.2 proof-utils.el
485c485
<       (replace-match ""))))
---
>       (replace-match proof-shell-insert-space-fudge))))
488c488
<   (proof-replace-regexp-in-string pg-special-char-regexp "" string))
---
>   (proof-replace-regexp-in-string pg-special-char-regexp proof-shell-insert-space-fudge string))

Here is an example:

ML {* Thread.fork (fn () =>
  (OS.Process.sleep (Time.fromSeconds 3); priority "urgent message"), []) *}

[Makarius]

The following somewhat adhoc modification of proof-shell-process-urgent-messages successfully works around the problem by placing the marker one more character to the left.

diff -c -r9.2 proof-shell.el
*** generic/proof-shell.el      6 Feb 2008 23:04:33 -0000       9.2
--- generic/proof-shell.el      14 Jun 2008 20:02:32 -0000
***************
*** 1388,1394 ****
          ;; should never be any such messages!
          ;; (max
          ;;  (marker-position proof-marker)
!             (- (point) proof-shell-eager-annotation-start-length)
          (1- (process-mark (get-buffer-process (current-buffer))))))
        ;; Otherwise, the search for the ending annotation was
        ;; unsuccessful, so we set the scanner marker to the start of
--- 1388,1394 ----
          ;; should never be any such messages!
          ;; (max
          ;;  (marker-position proof-marker)
!             (- (point) (1+ proof-shell-eager-annotation-start-length))
          (1- (process-mark (get-buffer-process (current-buffer))))))
        ;; Otherwise, the search for the ending annotation was
        ;; unsuccessful, so we set the scanner marker to the start of

[Makarius]

Just one more strange idea. How about displacing markers consistently by an offset of -1? Maybe this would also allow to get rid of proof-shell-insert-space-fudge.

[David Aspinall]

Many thanks for diagnosing this problem. The minimal patch is in CVS now, hopefully some Coq users will smoke test.