diff options
| author | David Aspinall | 2008-07-10 12:49:32 +0000 |
|---|---|---|
| committer | David Aspinall | 2008-07-10 12:49:32 +0000 |
| commit | 7a4b243be9784abd3b9b1171532b1e880ec43170 (patch) | |
| tree | 37de5f6b5e6e9eafed5294ce5498a33567aa769a /generic/proof-shell.el | |
| parent | 6dd4105c9088f8567cbb2d576461251b74c05c5e (diff) | |
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
Diffstat (limited to 'generic/proof-shell.el')
| -rw-r--r-- | generic/proof-shell.el | 2 |
1 files changed, 1 insertions, 1 deletions
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 |