aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEnrico Tassi2015-07-11 23:49:31 +0200
committerEnrico Tassi2015-07-11 23:50:01 +0200
commit7351bf1c179c4feebf4d93437625ea358dc59420 (patch)
treee08ae369c4dc74c54dad79a8c4d9c4c5fa2df761
parent31ce6ad3ca351b4742f66ed059356191ae96a3ac (diff)
CoqIDE: recenter on backtrack (Close: #4277)
-rw-r--r--ide/coqOps.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 2387d65c30..c6d3149475 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -669,7 +669,10 @@ object(self)
push_info "Coq is undoing" in
let conclusion () =
pop_info ();
- if move_insert then buffer#place_cursor ~where:self#get_start_of_input;
+ if move_insert then begin
+ buffer#place_cursor ~where:self#get_start_of_input;
+ script#recenter_insert;
+ end;
let start = self#get_start_of_input in
let stop = self#get_end_of_input in
Minilib.log(Printf.sprintf "cleanup tags %d %d" start#offset stop#offset);