From 2826683746569b9d78aa01e319315ab554e1619b Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 19:36:45 +0200 Subject: Fix omitted labels in function calls --- ide/coqOps.ml | 16 ++++++++-------- ide/coqide.ml | 10 +++++----- ide/ide_slave.ml | 2 +- ide/ideutils.ml | 2 +- ide/preferences.ml | 20 ++++++++++---------- ide/session.ml | 12 ++++++------ ide/wg_Command.ml | 6 +++--- ide/wg_Completion.ml | 26 +++++++++++++------------- ide/wg_Find.ml | 6 +++--- ide/wg_ProofView.ml | 6 +++--- ide/wg_ScriptView.ml | 4 ++-- ide/wg_Segment.ml | 6 +++--- 12 files changed, 58 insertions(+), 58 deletions(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 222b9eed9f..259557f407 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 = diff --git a/ide/coqide.ml b/ide/coqide.ml index 25858acced..0b7567a5ae 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/ide_slave.ml b/ide/ide_slave.ml index bf86db08ff..ca0ef38d32 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. * diff --git a/ide/ideutils.ml b/ide/ideutils.ml index da867e689e..d7d38a5ec2 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -58,7 +58,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 f0fd45d77f..e1fc4005ba 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:"" ~repr:Repr.(string) @@ -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 6262820e7b..7aea75ac84 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 3fcb7ce49e..621c46b94a 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 aeae3e1fdb..3bb6b780e6 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_Find.ml b/ide/wg_Find.ml index 3d847ddcc1..f84b9063bf 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_ProofView.ml b/ide/wg_ProofView.ml index 3cbe583881..f801091cfc 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 218cedb363..7c058febd3 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -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 dbc1740ef6..d527a0d13a 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 -> () -- cgit v1.2.3 From f67f84fc4831923aa9a2323b3a71c3a69fe61480 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 19:50:27 +0200 Subject: Use [method!] to override methods (warning 7) --- ide/preferences.ml | 2 +- ide/wg_Detachable.ml | 4 ++-- ide/wg_Notebook.ml | 2 +- ide/wg_ScriptView.ml | 8 ++++---- 4 files changed, 8 insertions(+), 8 deletions(-) (limited to 'ide') diff --git a/ide/preferences.ml b/ide/preferences.ml index e1fc4005ba..9fe9c6337d 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -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 *) diff --git a/ide/wg_Detachable.ml b/ide/wg_Detachable.ml index 3d1b63dfae..cbc34462e2 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_Notebook.ml b/ide/wg_Notebook.ml index 08d7d19833..0e5284c2f9 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_ScriptView.ml b/ide/wg_ScriptView.ml index 7c058febd3..7430f07d47 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; -- cgit v1.2.3 From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 20:04:58 +0200 Subject: Remove some unused values and types --- ide/coqOps.ml | 3 --- ide/ideutils.ml | 11 ----------- 2 files changed, 14 deletions(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 259557f407..b180aa5569 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -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) diff --git a/ide/ideutils.ml b/ide/ideutils.ml index d7d38a5ec2..a08ab07b5f 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 -- cgit v1.2.3 From b20d52da0d040fe37bb75b0b739ad7686f9af127 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Sat, 22 Apr 2017 12:55:46 +0200 Subject: Warning 29: non escaped end of line may be non portable --- ide/coqide_ui.ml | 284 +++++++++++++++++++++++++++---------------------------- ide/ide_slave.ml | 4 +- 2 files changed, 144 insertions(+), 144 deletions(-) (limited to 'ide') diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index 2ae18593ac..91c281c8d8 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 " - - - - - - - - - - - - - - - - - - - %s - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - %s - - - - - - - - - - - %s - - - - - - - - - - %s - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -" + let theui = Printf.sprintf "\ +\n\ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n %s\ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n %s\ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n %s\ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n %s\ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n\ +\n\ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n \ +\n\ +\n" (if Coq_config.gtk_platform <> `QUARTZ then "" 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 ca0ef38d32..dbfe4256b3 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -512,5 +512,5 @@ let () = Coqtop.toploop_init := (fun 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" -- cgit v1.2.3 From 5eb09af1e3686d6ac518b9eafe7cfcebd2b16375 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Tue, 25 Apr 2017 14:03:54 +0200 Subject: Remove uses of [Flags.make_silent] --- ide/ide_slave.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index dbfe4256b3..966a94da91 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -505,7 +505,7 @@ 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) -- cgit v1.2.3