aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqOps.ml
diff options
context:
space:
mode:
authorGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-21 19:36:45 +0200
committerGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-27 21:33:39 +0200
commit2826683746569b9d78aa01e319315ab554e1619b (patch)
treeda0933c7169635d9e35003af4d40b0408e7de96d /ide/coqOps.ml
parent8a3cd2fe699540f1ae5a56917d0f6b951f81d731 (diff)
Fix omitted labels in function calls
Diffstat (limited to 'ide/coqOps.ml')
-rw-r--r--ide/coqOps.ml16
1 files changed, 8 insertions, 8 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 222b9eed9..259557f40 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -117,7 +117,7 @@ end = struct
(b#get_iter_at_mark s.start)#offset
(b#get_iter_at_mark s.stop)#offset
(ellipsize
- ((b#get_iter_at_mark s.start)#get_slice (b#get_iter_at_mark s.stop)))
+ ((b#get_iter_at_mark s.start)#get_slice ~stop:(b#get_iter_at_mark s.stop)))
(String.concat "," (List.map str_of_flag s.flags))
(ellipsize
(String.concat ","
@@ -207,7 +207,7 @@ object (self)
in
List.iter (fun s -> set_index s (s.index + 1)) after;
set_index s (document_length - List.length after);
- ignore ((SentenceId.connect s)#changed self#on_changed);
+ ignore ((SentenceId.connect s)#changed ~callback:self#on_changed);
document_length <- document_length + 1;
List.iter (fun f -> f `INSERT) cbs
@@ -221,8 +221,8 @@ object (self)
List.iter (fun f -> f `REMOVE) cbs
initializer
- let _ = (Doc.connect doc)#pushed self#on_push in
- let _ = (Doc.connect doc)#popped self#on_pop in
+ let _ = (Doc.connect doc)#pushed ~callback:self#on_push in
+ let _ = (Doc.connect doc)#popped ~callback:self#on_pop in
()
end
@@ -273,15 +273,15 @@ object(self)
else iter
in
let iter = sentence_start iter in
- script#buffer#place_cursor iter;
+ script#buffer#place_cursor ~where:iter;
ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter)
in
- let _ = segment#connect#clicked on_click in
+ let _ = segment#connect#clicked ~callback:on_click in
()
method private tooltip_callback ~x ~y ~kbd tooltip =
- let x, y = script#window_to_buffer_coords `WIDGET x y in
- let iter = script#get_iter_at_location x y in
+ let x, y = script#window_to_buffer_coords ~tag:`WIDGET ~x ~y in
+ let iter = script#get_iter_at_location ~x ~y in
if iter#has_tag Tags.Script.tooltip then begin
let s =
let rec aux iter =