Handle paste to beginning of buffer correctly. #15939
Conversation
jfehrle
added
kind: fix
jfehrle
force-pushed
the
pmp_begin_buffer
branch
from
d39ed0c
to
2d2cd6e
Compare
ide/coqide/session.ml
Outdated
| let () = List.iter (fun mark -> | ||
| try match mark with | ||
| | `Mark mark -> buffer#delete_mark (`MARK mark) | ||
| | `Begin -> let action = Coq.seq (coqops#backtrack_to_begin ()) |
There was a problem hiding this comment.
Why don't you simply use handle_reset_initial there? I think it's precisely behaving like this piece of code.
There was a problem hiding this comment.
Calling handle_reset_initial gives the error "Already initialized" from Idetop.init. Calling Coq.reset_coqtop works, but it doesn't correctly clear breakpoints in the replaced part of the buffer. I'd rather not tie this code to breakpoints, at least for now.
ide/coqide/session.ml
Outdated
| @@ -118,7 +118,9 @@ let create_script coqtop source_buffer = | |||
|
|
|||
| let misc () = CDebug.(get_flag misc) | |||
|
|
|||
| type action_stack = Gtk.text_mark list option | |||
| type action_stack_entry = [ | `Mark of Gtk.text_mark | `Begin ] | |||
There was a problem hiding this comment.
Don't use algebraic variants, they have a lot of issues. Either use the option type or remove the backquotes from these constructors.
There was a problem hiding this comment.
Got it. The OCaml doc doesn't explain algebraic variants very well. Or for that matter, type inference.
jfehrle
force-pushed
the
pmp_begin_buffer
branch
from
2d2cd6e
to
cac6f8f
Compare
|
Updated. Couldn't we avoid using marks entirely by instead finding the smallest changed offset in the buffer in |
|
I tried using backtrack_to_iter recently to fix this set of issues but I didn't manage to make it work properly. Iters have a strong tendency to get invalidated under your feet. |
|
In this case, compute the offset and create an iterator from it just before calling backtrack_to_iter. |
|
@coqbot merge now |
Fixes #15882
The cause is similar to that of #15861. When the entire buffer is replaced with a paste, the buffer is emptied and all the marks disappear, therefore a different approach is needed.
Not very elegant; IMHO the marks are not a great fit for the test.
@Alitzer Would you test this, too? I tried the cases I could think of--not many.