From 6d1e0f80d215678559ada3d5b32c22c0d015454e Mon Sep 17 00:00:00 2001
From: Xavier Leroy
Date: Sun, 14 Aug 2016 18:03:22 +0200
Subject: Fix regression in Coqide's "forward one command" command

In Coqide 8.5pl2, "forward one command" (down arrow) always repositions the insertion point at the end of the phrase being executed, just after the final ".".

In Coqide 8.4, the insertion point is not moved if it is after the end of the executed phrase.  The insertion point is moved only if it falls behind the phrase being executed.

I find the 8.5 behavior to be a regression over the lot more useful 8.4 behavior.  This commit restores the 8.4 behavior of "forward one command".
---
 ide/coqOps.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'ide')

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 80ce99a69e..e12fda9141 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -338,8 +338,11 @@ object(self)
   method private show_goals_aux ?(move_insert=false) () =
     Coq.PrintOpt.set_printing_width proof#width;
     if move_insert then begin
-      buffer#place_cursor ~where:self#get_start_of_input;
-      script#recenter_insert;
+      let dest = self#get_start_of_input in
+      if (buffer#get_iter_at_mark `INSERT)#compare dest <= 0 then begin
+        buffer#place_cursor ~where:dest;
+        script#recenter_insert
+      end
     end;
     Coq.bind (Coq.goals ~logger:messages#push ()) (function
     | Fail x -> self#handle_failure_aux ~move_insert x
-- 
cgit v1.2.3