diff options
Diffstat (limited to 'ide')
-rw-r--r-- | ide/coqOps.ml | 19 | ||||
-rw-r--r-- | ide/coqide.ml | 10 | ||||
-rw-r--r-- | ide/coqide_ui.ml | 284 | ||||
-rw-r--r-- | ide/ide_slave.ml | 8 | ||||
-rw-r--r-- | ide/ideutils.ml | 13 | ||||
-rw-r--r-- | ide/preferences.ml | 22 | ||||
-rw-r--r-- | ide/session.ml | 12 | ||||
-rw-r--r-- | ide/wg_Command.ml | 6 | ||||
-rw-r--r-- | ide/wg_Completion.ml | 26 | ||||
-rw-r--r-- | ide/wg_Detachable.ml | 4 | ||||
-rw-r--r-- | ide/wg_Find.ml | 6 | ||||
-rw-r--r-- | ide/wg_Notebook.ml | 2 | ||||
-rw-r--r-- | ide/wg_ProofView.ml | 6 | ||||
-rw-r--r-- | ide/wg_ScriptView.ml | 12 | ||||
-rw-r--r-- | ide/wg_Segment.ml | 6 |
15 files changed, 211 insertions, 225 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 222b9eed9..b180aa556 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 "," @@ -128,9 +128,6 @@ end = struct end open SentenceId -let log_pp msg : unit task = - Coq.lift (fun () -> Minilib.log_pp msg) - let log msg : unit task = Coq.lift (fun () -> Minilib.log msg) @@ -207,7 +204,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 +218,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 +270,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 = diff --git a/ide/coqide.ml b/ide/coqide.ml index 25858acce..0b7567a5a 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -792,11 +792,11 @@ let coqtop_arguments sn = sn.messages#push Feedback.Error (Pp.str msg) else dialog#destroy () in - let _ = entry#connect#activate ok_cb in - let _ = ok#connect#clicked ok_cb in + let _ = entry#connect#activate ~callback:ok_cb in + let _ = ok#connect#clicked ~callback:ok_cb in let cancel = GButton.button ~stock:`CANCEL ~packing:box#add () in let cancel_cb () = dialog#destroy () in - let _ = cancel#connect#clicked cancel_cb in + let _ = cancel#connect#clicked ~callback:cancel_cb in dialog#show () let coqtop_arguments = cb_on_current_term coqtop_arguments @@ -1274,8 +1274,8 @@ let build_ui () = if b then toolbar#misc#show () else toolbar#misc#hide () in stick show_toolbar toolbar refresh_toolbar; - let _ = source_style#connect#changed refresh_style in - let _ = source_language#connect#changed refresh_language in + let _ = source_style#connect#changed ~callback:refresh_style in + let _ = source_language#connect#changed ~callback:refresh_language in (* Color configuration *) Tags.Script.incomplete#set_property diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index 2ae18593a..91c281c8d 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -28,148 +28,148 @@ let list_queries menu li = res_buf let init () = - let theui = Printf.sprintf "<ui> -<menubar name='CoqIde MenuBar'> - <menu action='File'> - <menuitem action='New' /> - <menuitem action='Open' /> - <menuitem action='Save' /> - <menuitem action='Save as' /> - <menuitem action='Save all' /> - <menuitem action='Revert all buffers' /> - <menuitem action='Close buffer' /> - <menuitem action='Print...' /> - <menu action='Export to'> - <menuitem action='Html' /> - <menuitem action='Latex' /> - <menuitem action='Dvi' /> - <menuitem action='Pdf' /> - <menuitem action='Ps' /> - </menu> - <menuitem action='Rehighlight' /> - %s - </menu> - <menu name='Edit' action='Edit'> - <menuitem action='Undo' /> - <menuitem action='Redo' /> - <separator /> - <menuitem action='Cut' /> - <menuitem action='Copy' /> - <menuitem action='Paste' /> - <separator /> - <menuitem action='Find' /> - <menuitem action='Find Next' /> - <menuitem action='Find Previous' /> - <menuitem action='Complete Word' /> - <separator /> - <menuitem action='External editor' /> - <separator /> - <menuitem name='Prefs' action='Preferences' /> - </menu> - <menu name='View' action='View'> - <menuitem action='Previous tab' /> - <menuitem action='Next tab' /> - <separator/> - <menuitem action='Zoom in' /> - <menuitem action='Zoom out' /> - <menuitem action='Zoom fit' /> - <separator/> - <menuitem action='Show Toolbar' /> - <menuitem action='Query Pane' /> - <separator/> - <menuitem action='Display implicit arguments' /> - <menuitem action='Display coercions' /> - <menuitem action='Display raw matching expressions' /> - <menuitem action='Display notations' /> - <menuitem action='Display all basic low-level contents' /> - <menuitem action='Display existential variable instances' /> - <menuitem action='Display universe levels' /> - <menuitem action='Display all low-level contents' /> - </menu> - <menu action='Navigation'> - <menuitem action='Forward' /> - <menuitem action='Backward' /> - <menuitem action='Go to' /> - <menuitem action='Start' /> - <menuitem action='End' /> - <menuitem action='Interrupt' /> - <menuitem action='Previous' /> - <menuitem action='Next' /> - </menu> - <menu action='Try Tactics'> - <menuitem action='auto' /> - <menuitem action='auto with *' /> - <menuitem action='eauto' /> - <menuitem action='eauto with *' /> - <menuitem action='intuition' /> - <menuitem action='omega' /> - <menuitem action='simpl' /> - <menuitem action='tauto' /> - <menuitem action='trivial' /> - <menuitem action='Wizard' /> - <separator /> - %s - </menu> - <menu action='Templates'> - <menuitem action='Lemma' /> - <menuitem action='Theorem' /> - <menuitem action='Definition' /> - <menuitem action='Inductive' /> - <menuitem action='Fixpoint' /> - <menuitem action='Scheme' /> - <menuitem action='match' /> - <separator /> - %s - </menu> - <menu action='Queries'> - <menuitem action='Search' /> - <menuitem action='Check' /> - <menuitem action='Print' /> - <menuitem action='About' /> - <menuitem action='Locate' /> - <menuitem action='Print Assumptions' /> - <separator /> - %s - </menu> - <menu name='Tools' action='Tools'> - <menuitem action='Comment' /> - <menuitem action='Uncomment' /> - <separator /> - <menuitem action='Coqtop arguments' /> - </menu> - <menu action='Compile'> - <menuitem action='Compile buffer' /> - <menuitem action='Make' /> - <menuitem action='Next error' /> - <menuitem action='Make makefile' /> - </menu> - <menu action='Windows'> - <menuitem action='Detach View' /> - </menu> - <menu name='Help' action='Help'> - <menuitem action='Browse Coq Manual' /> - <menuitem action='Browse Coq Library' /> - <menuitem action='Help for keyword' /> - <menuitem action='Help for μPG mode' /> - <separator /> - <menuitem name='Abt' action='About Coq' /> - </menu> -</menubar> -<toolbar name='CoqIde ToolBar'> - <toolitem action='Save' /> - <toolitem action='Close buffer' /> - <toolitem action='Forward' /> - <toolitem action='Backward' /> - <toolitem action='Go to' /> - <toolitem action='Start' /> - <toolitem action='End' /> - <toolitem action='Force' /> - <toolitem action='Interrupt' /> - <toolitem action='Previous' /> - <toolitem action='Next' /> - <toolitem action='Wizard' /> -</toolbar> -</ui>" + let theui = Printf.sprintf "<ui>\ +\n<menubar name='CoqIde MenuBar'>\ +\n <menu action='File'>\ +\n <menuitem action='New' />\ +\n <menuitem action='Open' />\ +\n <menuitem action='Save' />\ +\n <menuitem action='Save as' />\ +\n <menuitem action='Save all' />\ +\n <menuitem action='Revert all buffers' />\ +\n <menuitem action='Close buffer' />\ +\n <menuitem action='Print...' />\ +\n <menu action='Export to'>\ +\n <menuitem action='Html' />\ +\n <menuitem action='Latex' />\ +\n <menuitem action='Dvi' />\ +\n <menuitem action='Pdf' />\ +\n <menuitem action='Ps' />\ +\n </menu>\ +\n <menuitem action='Rehighlight' />\ +\n %s\ +\n </menu>\ +\n <menu name='Edit' action='Edit'>\ +\n <menuitem action='Undo' />\ +\n <menuitem action='Redo' />\ +\n <separator />\ +\n <menuitem action='Cut' />\ +\n <menuitem action='Copy' />\ +\n <menuitem action='Paste' />\ +\n <separator />\ +\n <menuitem action='Find' />\ +\n <menuitem action='Find Next' />\ +\n <menuitem action='Find Previous' />\ +\n <menuitem action='Complete Word' />\ +\n <separator />\ +\n <menuitem action='External editor' />\ +\n <separator />\ +\n <menuitem name='Prefs' action='Preferences' />\ +\n </menu>\ +\n <menu name='View' action='View'>\ +\n <menuitem action='Previous tab' />\ +\n <menuitem action='Next tab' />\ +\n <separator/>\ +\n <menuitem action='Zoom in' />\ +\n <menuitem action='Zoom out' />\ +\n <menuitem action='Zoom fit' />\ +\n <separator/>\ +\n <menuitem action='Show Toolbar' />\ +\n <menuitem action='Query Pane' />\ +\n <separator/>\ +\n <menuitem action='Display implicit arguments' />\ +\n <menuitem action='Display coercions' />\ +\n <menuitem action='Display raw matching expressions' />\ +\n <menuitem action='Display notations' />\ +\n <menuitem action='Display all basic low-level contents' />\ +\n <menuitem action='Display existential variable instances' />\ +\n <menuitem action='Display universe levels' />\ +\n <menuitem action='Display all low-level contents' />\ +\n </menu>\ +\n <menu action='Navigation'>\ +\n <menuitem action='Forward' />\ +\n <menuitem action='Backward' />\ +\n <menuitem action='Go to' />\ +\n <menuitem action='Start' />\ +\n <menuitem action='End' />\ +\n <menuitem action='Interrupt' />\ +\n <menuitem action='Previous' />\ +\n <menuitem action='Next' />\ +\n </menu>\ +\n <menu action='Try Tactics'>\ +\n <menuitem action='auto' />\ +\n <menuitem action='auto with *' />\ +\n <menuitem action='eauto' />\ +\n <menuitem action='eauto with *' />\ +\n <menuitem action='intuition' />\ +\n <menuitem action='omega' />\ +\n <menuitem action='simpl' />\ +\n <menuitem action='tauto' />\ +\n <menuitem action='trivial' />\ +\n <menuitem action='Wizard' />\ +\n <separator />\ +\n %s\ +\n </menu>\ +\n <menu action='Templates'>\ +\n <menuitem action='Lemma' />\ +\n <menuitem action='Theorem' />\ +\n <menuitem action='Definition' />\ +\n <menuitem action='Inductive' />\ +\n <menuitem action='Fixpoint' />\ +\n <menuitem action='Scheme' />\ +\n <menuitem action='match' />\ +\n <separator />\ +\n %s\ +\n </menu>\ +\n <menu action='Queries'>\ +\n <menuitem action='Search' />\ +\n <menuitem action='Check' />\ +\n <menuitem action='Print' />\ +\n <menuitem action='About' />\ +\n <menuitem action='Locate' />\ +\n <menuitem action='Print Assumptions' />\ +\n <separator />\ +\n %s\ +\n </menu>\ +\n <menu name='Tools' action='Tools'>\ +\n <menuitem action='Comment' />\ +\n <menuitem action='Uncomment' />\ +\n <separator />\ +\n <menuitem action='Coqtop arguments' />\ +\n </menu>\ +\n <menu action='Compile'>\ +\n <menuitem action='Compile buffer' />\ +\n <menuitem action='Make' />\ +\n <menuitem action='Next error' />\ +\n <menuitem action='Make makefile' />\ +\n </menu>\ +\n <menu action='Windows'>\ +\n <menuitem action='Detach View' />\ +\n </menu>\ +\n <menu name='Help' action='Help'>\ +\n <menuitem action='Browse Coq Manual' />\ +\n <menuitem action='Browse Coq Library' />\ +\n <menuitem action='Help for keyword' />\ +\n <menuitem action='Help for μPG mode' />\ +\n <separator />\ +\n <menuitem name='Abt' action='About Coq' />\ +\n </menu>\ +\n</menubar>\ +\n<toolbar name='CoqIde ToolBar'>\ +\n <toolitem action='Save' />\ +\n <toolitem action='Close buffer' />\ +\n <toolitem action='Forward' />\ +\n <toolitem action='Backward' />\ +\n <toolitem action='Go to' />\ +\n <toolitem action='Start' />\ +\n <toolitem action='End' />\ +\n <toolitem action='Force' />\ +\n <toolitem action='Interrupt' />\ +\n <toolitem action='Previous' />\ +\n <toolitem action='Next' />\ +\n <toolitem action='Wizard' />\ +\n</toolbar>\ +\n</ui>" (if Coq_config.gtk_platform <> `QUARTZ then "<menuitem action='Quit' />" else "") (Buffer.contents (list_items "Tactic" Coq_commands.tactics)) (Buffer.contents (list_items "Template" Coq_commands.commands)) diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index bf86db08f..966a94da9 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -82,7 +82,7 @@ let add ((s,eid),(sid,verbose)) = let loc_ast = Stm.parse_sentence sid pa in let newid, rc = Stm.add ~ontop:sid verbose loc_ast in let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in - ide_cmd_checks newid loc_ast; + ide_cmd_checks ~id:newid loc_ast; (* TODO: the "" parameter is a leftover of the times the protocol * used to include stderr/stdout output. * @@ -505,12 +505,12 @@ let rec parse = function let () = Coqtop.toploop_init := (fun args -> let args = parse args in - Flags.make_silent true; + Flags.quiet := true; CoqworkmgrApi.(init Flags.High); args) let () = Coqtop.toploop_run := loop let () = Usage.add_to_usage "coqidetop" -" --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format - --help-XML-protocol print the documentation of the XML protocol used by CoqIDE\n" +" --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\ +\n --help-XML-protocol print the documentation of the XML protocol used by CoqIDE\n" diff --git a/ide/ideutils.ml b/ide/ideutils.ml index da867e689..a08ab07b5 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -35,17 +35,6 @@ let flash_info = let flash_context = status#new_context ~name:"Flash" in (fun ?(delay=5000) s -> flash_context#flash ~delay s) -let xml_to_string xml = - let open Xml_datatype in - let buf = Buffer.create 1024 in - let rec iter = function - | PCData s -> Buffer.add_string buf s - | Element (_, _, children) -> - List.iter iter children - in - let () = iter xml in - Buffer.contents buf - let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text = (** FIXME: LablGTK2 does not export the C insert_with_tags function, so that it has to reimplement its own helper function. Unluckily, it relies on @@ -58,7 +47,7 @@ let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text = let () = buf#insert ~iter:(buf#get_iter_at_mark mark) text in let start = buf#get_iter_at_mark mark in let stop = buf#get_iter_at_mark rmark in - let iter tag = buf#apply_tag tag start stop in + let iter tag = buf#apply_tag tag ~start ~stop in List.iter iter tags let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg = diff --git a/ide/preferences.ml b/ide/preferences.ml index f0fd45d77..9fe9c6337 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -73,8 +73,8 @@ end let stick (pref : 'a preference) (obj : #GObj.widget as 'obj) (cb : 'a -> unit) = let _ = cb pref#get in - let p_id = pref#connect#changed (fun v -> cb v) in - let _ = obj#misc#connect#destroy (fun () -> pref#connect#disconnect p_id) in + let p_id = pref#connect#changed ~callback:(fun v -> cb v) in + let _ = obj#misc#connect#destroy ~callback:(fun () -> pref#connect#disconnect p_id) in () (** Useful marshallers *) @@ -314,7 +314,7 @@ let attach_modifiers (pref : string preference) prefix = in GtkData.AccelMap.foreach change in - pref#connect#changed cb + pref#connect#changed ~callback:cb let modifier_for_navigation = new preference ~name:["modifier_for_navigation"] ~init:"<Control>" ~repr:Repr.(string) @@ -360,7 +360,7 @@ object ~name:["doc_url"] ~init:Coq_config.wwwrefman ~repr:Repr.(string) as super - method set v = + method! set v = if not (Flags.is_standard_doc_url v) && v <> use_default_doc_url && (* Extra hack to support links to last released doc version *) @@ -408,10 +408,10 @@ let background_color = new preference ~name:["background_color"] ~init:"cornsilk" ~repr:Repr.(string) let attach_bg (pref : string preference) (tag : GText.tag) = - pref#connect#changed (fun c -> tag#set_property (`BACKGROUND c)) + pref#connect#changed ~callback:(fun c -> tag#set_property (`BACKGROUND c)) let attach_fg (pref : string preference) (tag : GText.tag) = - pref#connect#changed (fun c -> tag#set_property (`FOREGROUND c)) + pref#connect#changed ~callback:(fun c -> tag#set_property (`FOREGROUND c)) let processing_color = new preference ~name:["processing_color"] ~init:"light blue" ~repr:Repr.(string) @@ -468,7 +468,7 @@ let create_tag name default = let iter table = let tag = GText.tag ~name () in table#add tag#as_tag; - ignore (pref#connect#changed (fun _ -> set_tag tag)); + ignore (pref#connect#changed ~callback:(fun _ -> set_tag tag)); set_tag tag; in List.iter iter [Tags.Script.table; Tags.Proof.table; Tags.Message.table]; @@ -601,8 +601,8 @@ object (self) box#pack italic#coerce; box#pack underline#coerce; let cb but obj = obj#set_sensitive (not but#active) in - let _ = fg_unset#connect#toggled (fun () -> cb fg_unset fg_color#misc) in - let _ = bg_unset#connect#toggled (fun () -> cb bg_unset bg_color#misc) in + let _ = fg_unset#connect#toggled ~callback:(fun () -> cb fg_unset fg_color#misc) in + let _ = bg_unset#connect#toggled ~callback:(fun () -> cb bg_unset bg_color#misc) in () end @@ -692,7 +692,7 @@ let configure ?(apply=(fun () -> ())) () = ~color:(Tags.color_of_string pref#get) ~packing:(table#attach ~left:1 ~top:i) () in - let _ = button#connect#color_set begin fun () -> + let _ = button#connect#color_set ~callback:begin fun () -> pref#set (Tags.string_of_color button#color) end in let reset _ = @@ -754,7 +754,7 @@ let configure ?(apply=(fun () -> ())) () = let button text (pref : bool preference) = let active = pref#get in let but = GButton.check_button ~label:text ~active ~packing:box#pack () in - ignore (but#connect#toggled (fun () -> pref#set but#active)) + ignore (but#connect#toggled ~callback:(fun () -> pref#set but#active)) in let () = button "Dynamic word wrap" dynamic_word_wrap in let () = button "Show line number" show_line_number in diff --git a/ide/session.ml b/ide/session.ml index 6262820e7..7aea75ac8 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -249,8 +249,8 @@ let make_table_widget ?sort cd cb = let () = data#set_headers_visible true in let () = data#set_headers_clickable true in let refresh clr = data#misc#modify_base [`NORMAL, `NAME clr] in - let _ = background_color#connect#changed refresh in - let _ = data#misc#connect#realize (fun () -> refresh background_color#get) in + let _ = background_color#connect#changed ~callback:refresh in + let _ = data#misc#connect#realize ~callback:(fun () -> refresh background_color#get) in let mk_rend c = GTree.cell_renderer_text [], ["text",c] in let cols = List.map2 (fun (_,c) (_,n,v) -> @@ -308,8 +308,8 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage = !callback errs; List.iter (fun (lno, msg) -> access (fun columns store -> let line = store#append () in - store#set line (find_int_col "Line" columns) lno; - store#set line (find_string_col "Error message" columns) msg)) + store#set ~row:line ~column:(find_int_col "Line" columns) lno; + store#set ~row:line ~column:(find_string_col "Error message" columns) msg)) errs end method on_update ~callback:cb = callback := cb @@ -348,8 +348,8 @@ let create_jobpage coqtop coqops : jobpage = else false) else let line = store#append () in - store#set line column id; - store#set line (find_string_col "Job name" columns) job)) + store#set ~row:line ~column id; + store#set ~row:line ~column:(find_string_col "Job name" columns) job)) jobs end method on_update ~callback:cb = callback := cb diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 3fcb7ce49..621c46b94 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -91,8 +91,8 @@ object(self) let result = GText.view ~packing:r_bin#add () in views <- (frame#coerce, result, combo#entry) :: views; let cb clr = result#misc#modify_base [`NORMAL, `NAME clr] in - let _ = background_color#connect#changed cb in - let _ = result#misc#connect#realize (fun () -> cb background_color#get) in + let _ = background_color#connect#changed ~callback:cb in + let _ = result#misc#connect#realize ~callback:(fun () -> cb background_color#get) in let cb ft = result#misc#modify_font (Pango.Font.from_string ft) in stick text_font result cb; result#misc#set_can_focus true; (* false causes problems for selection *) @@ -165,7 +165,7 @@ object(self) self#new_page_maker; self#new_query_aux ~grab_now:false (); frame#misc#hide (); - let _ = background_color#connect#changed self#refresh_color in + let _ = background_color#connect#changed ~callback:self#refresh_color in self#refresh_color background_color#get; ignore(notebook#event#connect#key_press ~callback:(fun ev -> if GdkEvent.Key.keyval ev = GdkKeysyms._Escape then (self#hide; true) diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index aeae3e1fd..3bb6b780e 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -154,7 +154,7 @@ object (self) let () = store#clear () in let iter prop = let iter = store#append () in - store#set iter column prop + store#set ~row:iter ~column prop in let () = current_completion <- (pref, props) in Proposals.iter iter props @@ -267,7 +267,7 @@ object (self) (** Position of view w.r.t. window *) let (ux, uy) = Gdk.Window.get_position view#misc#window in (** Relative buffer position to view *) - let (dx, dy) = view#window_to_buffer_coords `WIDGET 0 0 in + let (dx, dy) = view#window_to_buffer_coords ~tag:`WIDGET ~x:0 ~y:0 in (** Iter position *) let iter = view#buffer#get_iter pos in let coords = view#get_iter_location iter in @@ -397,11 +397,11 @@ object (self) let () = self#select_first () in let () = obj#misc#show () in let () = self#manage_scrollbar () in - obj#resize 1 1 + obj#resize ~width:1 ~height:1 method private start_callback off = let (x, y, w, h) = self#coordinates (`OFFSET off) in - let () = obj#move x (y + 3 * h / 2) in + let () = obj#move ~x ~y:(y + 3 * h / 2) in () method private update_callback (off, word, props) = @@ -433,21 +433,21 @@ object (self) else false in (** Style handling *) - let _ = view#misc#connect#style_set self#refresh_style in + let _ = view#misc#connect#style_set ~callback:self#refresh_style in let _ = self#refresh_style () in let _ = data#set_resize_mode `PARENT in let _ = frame#set_resize_mode `PARENT in (** Callback to model *) - let _ = model#connect#start_completion self#start_callback in - let _ = model#connect#update_completion self#update_callback in - let _ = model#connect#end_completion self#end_callback in + let _ = model#connect#start_completion ~callback:self#start_callback in + let _ = model#connect#update_completion ~callback:self#update_callback in + let _ = model#connect#end_completion ~callback:self#end_callback in (** Popup interaction *) - let _ = view#event#connect#key_press key_cb in + let _ = view#event#connect#key_press ~callback:key_cb in (** Hiding the popup when necessary*) - let _ = view#misc#connect#hide obj#misc#hide in - let _ = view#event#connect#button_press (fun _ -> self#hide (); false) in - let _ = view#connect#move_cursor move_cb in - let _ = view#event#connect#focus_out (fun _ -> self#hide (); false) in + let _ = view#misc#connect#hide ~callback:obj#misc#hide in + let _ = view#event#connect#button_press ~callback:(fun _ -> self#hide (); false) in + let _ = view#connect#move_cursor ~callback:move_cb in + let _ = view#event#connect#focus_out ~callback:(fun _ -> self#hide (); false) in () end diff --git a/ide/wg_Detachable.ml b/ide/wg_Detachable.ml index 3d1b63dfa..cbc34462e 100644 --- a/ide/wg_Detachable.ml +++ b/ide/wg_Detachable.ml @@ -26,8 +26,8 @@ class detachable (obj : ([> Gtk.box] as 'a) Gobject.obj) = val mutable attached_cb = (fun _ -> ()) method child = frame#child - method add = frame#add - method pack ?from ?expand ?fill ?padding w = + method! add = frame#add + method! pack ?from ?expand ?fill ?padding w = if frame#all_children = [] then self#add w else raise (Invalid_argument "detachable#pack") diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml index 3d847ddcc..f84b9063b 100644 --- a/ide/wg_Find.ml +++ b/ide/wg_Find.ml @@ -186,8 +186,8 @@ class finder name (view : GText.view) = in let find_cb = generic_cb self#hide self#find_forward in let replace_cb = generic_cb self#hide self#replace in - let _ = find_entry#event#connect#key_press find_cb in - let _ = replace_entry#event#connect#key_press replace_cb in + let _ = find_entry#event#connect#key_press ~callback:find_cb in + let _ = replace_entry#event#connect#key_press ~callback:replace_cb in (** TextView interaction *) let view_cb ev = @@ -197,7 +197,7 @@ class finder name (view : GText.view) = else false else false in - let _ = view#event#connect#key_press view_cb in + let _ = view#event#connect#key_press ~callback:view_cb in () end diff --git a/ide/wg_Notebook.ml b/ide/wg_Notebook.ml index 08d7d1983..0e5284c2f 100644 --- a/ide/wg_Notebook.ml +++ b/ide/wg_Notebook.ml @@ -50,7 +50,7 @@ object(self) method pages = term_list - method remove_page index = + method! remove_page index = term_list <- Util.List.filteri (fun i x -> if i = index then kill_page x; i <> index) term_list; super#remove_page index diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 3cbe58388..f801091cf 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -188,8 +188,8 @@ let proof_view () = let default_clipboard = GData.clipboard Gdk.Atom.primary in let _ = buffer#add_selection_clipboard default_clipboard in let cb clr = view#misc#modify_base [`NORMAL, `NAME clr] in - let _ = background_color#connect#changed cb in - let _ = view#misc#connect#realize (fun () -> cb background_color#get) in + let _ = background_color#connect#changed ~callback:cb in + let _ = view#misc#connect#realize ~callback:(fun () -> cb background_color#get) in let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in stick text_font view cb; @@ -226,5 +226,5 @@ let proof_view () = (* Is there a better way to connect the signal ? *) (* Can this be done in the object constructor? *) let w_cb _ = pf#refresh ~force:false in - ignore (view#misc#connect#size_allocate w_cb); + ignore (view#misc#connect#size_allocate ~callback:w_cb); pf diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 218cedb36..7430f07d4 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -301,28 +301,28 @@ object (self) ~use_align:false ~yalign:0.75 ~within_margin:0.25 `INSERT (* HACK: missing gtksourceview features *) - method right_margin_position = + method! right_margin_position = let prop = { Gobject.name = "right-margin-position"; conv = Gobject.Data.int; } in Gobject.get prop obj - method set_right_margin_position pos = + method! set_right_margin_position pos = let prop = { Gobject.name = "right-margin-position"; conv = Gobject.Data.int; } in Gobject.set prop obj pos - method show_right_margin = + method! show_right_margin = let prop = { Gobject.name = "show-right-margin"; conv = Gobject.Data.boolean; } in Gobject.get prop obj - method set_show_right_margin show = + method! set_show_right_margin show = let prop = { Gobject.name = "show-right-margin"; conv = Gobject.Data.boolean; @@ -460,8 +460,8 @@ object (self) let _ = GtkSignal.connect ~sgn:move_line_signal ~callback obj in (** Plug on preferences *) let cb clr = self#misc#modify_base [`NORMAL, `NAME clr] in - let _ = background_color#connect#changed cb in - let _ = self#misc#connect#realize (fun () -> cb background_color#get) in + let _ = background_color#connect#changed ~callback:cb in + let _ = self#misc#connect#realize ~callback:(fun () -> cb background_color#get) in let cb b = self#set_wrap_mode (if b then `WORD else `NONE) in stick dynamic_word_wrap self cb; diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml index dbc1740ef..d527a0d13 100644 --- a/ide/wg_Segment.ml +++ b/ide/wg_Segment.ml @@ -75,7 +75,7 @@ object (self) self#redraw (); end in - let _ = box#misc#connect#size_allocate cb in + let _ = box#misc#connect#size_allocate ~callback:cb in let clicked_cb ev = match model with | None -> true | Some md -> @@ -86,7 +86,7 @@ object (self) let () = clicked#call idx in true in - let _ = eventbox#event#connect#button_press clicked_cb in + let _ = eventbox#event#connect#button_press ~callback:clicked_cb in let cb show = if show then self#misc#show () else self#misc#hide () in stick show_progress_bar self cb; (** Initial pixmap *) @@ -102,7 +102,7 @@ object (self) | `SET (i, color) -> if self#misc#visible then self#fill_range color i (i + 1) in - md#changed changed_cb + md#changed ~callback:changed_cb method private fill_range color i j = match model with | None -> () |