aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHugo Herbelin2020-04-22 22:37:13 +0200
committerHugo Herbelin2020-04-22 22:37:13 +0200
commit99dc43029b743412be3ad8b597a38bdd135e2e9c (patch)
tree389a23824d39c350b7319d43a73dd4f3172f3453
parent7e2167f5bfd7d70847d1b1ece34c1f0303f46fc8 (diff)
CoqIDE: Avoid invalidation of an iterator in insert callback.
This hopefully fix the segfaults we observe with completion.
-rw-r--r--ide/session.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/session.ml b/ide/session.ml
index b16af9c317..09391b7f50 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -151,7 +151,7 @@ let set_buffer_handlers
else if it#has_tag Tags.Script.processed then Some old
else if it#has_tag Tags.Script.error_bg then aux it it#backward_char
else None in
- aux it it in
+ aux it it#copy in
let insert_cb it s = if String.length s = 0 then () else begin
Minilib.log ("insert_cb " ^ string_of_int it#offset);
let text_mark = add_mark it in