diff options
| author | Enrico Tassi | 2015-07-11 23:49:31 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-07-11 23:50:01 +0200 |
| commit | 7351bf1c179c4feebf4d93437625ea358dc59420 (patch) | |
| tree | e08ae369c4dc74c54dad79a8c4d9c4c5fa2df761 | |
| parent | 31ce6ad3ca351b4742f66ed059356191ae96a3ac (diff) | |
CoqIDE: recenter on backtrack (Close: #4277)
| -rw-r--r-- | ide/coqOps.ml | 5 |
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); |
