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".

1 files changed, 5 insertions, 2 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 80ce99a69..e12fda914 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