From 7a4b243be9784abd3b9b1171532b1e880ec43170 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 10 Jul 2008 12:49:32 +0000
Subject: Minimal patch for Sledgehammer problem with Isabelle. Credit due to
 Makarius.  Tested *very briefly* with Coq. See
 http://proofgeneral.inf.ed.ac.uk/trac/ticket/200

---
 generic/proof-shell.el | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'generic')

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 20117797..7eeb6478 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1388,7 +1388,7 @@ This is a subroutine of `proof-shell-filter'."
 	  ;; should never be any such messages!
 	  ;; (max
 	  ;;  (marker-position proof-marker)
-	      (- (point) proof-shell-eager-annotation-start-length)
+	      (- (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
-- 
cgit v1.2.3