From 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 17 Sep 2009 15:58:14 +0000 Subject: Delete trailing whitespaces in all *.{v,ml*} files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/utils/configwin.mli | 2 +- ide/utils/configwin_ihm.ml | 24 ++++++------ ide/utils/configwin_keys.ml | 50 ++++++++++++------------ ide/utils/configwin_types.ml | 6 +-- ide/utils/editable_cells.ml | 92 ++++++++++++++++++++++---------------------- ide/utils/okey.mli | 64 +++++++++++++++--------------- 6 files changed, 119 insertions(+), 119 deletions(-) (limited to 'ide/utils') diff --git a/ide/utils/configwin.mli b/ide/utils/configwin.mli index 2d4dd4a78..386ef82af 100644 --- a/ide/utils/configwin.mli +++ b/ide/utils/configwin.mli @@ -248,7 +248,7 @@ val hotkey : ?editable: bool -> ?expand: bool -> ?help: string -> val modifiers : ?editable: bool -> ?expand: bool -> ?help: string -> ?allow:(Gdk.Tags.modifier list) -> - ?f: (Gdk.Tags.modifier list -> unit) -> + ?f: (Gdk.Tags.modifier list -> unit) -> string -> Gdk.Tags.modifier list -> parameter_kind (** [custom box f expand] creates a custom parameter, with diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml index 3ab3823de..ff74a3c33 100644 --- a/ide/utils/configwin_ihm.ml +++ b/ide/utils/configwin_ihm.ml @@ -810,13 +810,13 @@ class modifiers_param_box param = () in let value = ref param.md_value in - let _ = + let _ = match param.md_help with None -> () | Some help -> let tooltips = GData.tooltips () in ignore (hbox#connect#destroy ~callback: tooltips#destroy); - tooltips#set_tip wev#coerce ~text: help ~privat: help + tooltips#set_tip wev#coerce ~text: help ~privat: help in let _ = we#set_text (Configwin_types.modifiers_to_string param.md_value) in let mods_we_care = param.md_allow in @@ -830,7 +830,7 @@ class modifiers_param_box param = we#set_text (Configwin_types.modifiers_to_string !value); false in - let _ = + let _ = if param.md_editable then ignore (we#event#connect#key_press capture) else @@ -1093,13 +1093,13 @@ let edit ?(with_apply=true) (fun conf_struct -> new configuration_box tooltips conf_struct wnote) conf_struct_list in - + if with_apply then dialog#add_button Configwin_messages.mApply `APPLY; - + dialog#add_button Configwin_messages.mOk `OK; dialog#add_button Configwin_messages.mCancel `CANCEL; - + let f_apply () = List.iter (fun param_box -> param_box#apply) list_param_box ; apply () @@ -1441,11 +1441,11 @@ let hotkey ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v = hk_expand = expand ; } -let modifiers - ?(editable=true) - ?(expand=true) - ?help - ?(allow=[`CONTROL;`SHIFT;`LOCK;`MOD1;`MOD1;`MOD2;`MOD3;`MOD4;`MOD5]) +let modifiers + ?(editable=true) + ?(expand=true) + ?help + ?(allow=[`CONTROL;`SHIFT;`LOCK;`MOD1;`MOD1;`MOD2;`MOD3;`MOD4;`MOD5]) ?(f=(fun _ -> ())) label v = Modifiers_param { @@ -1456,7 +1456,7 @@ let modifiers md_f_apply = f ; md_expand = expand ; md_allow = allow ; - } + } (** Create a custom param.*) let custom ?label box f expand = diff --git a/ide/utils/configwin_keys.ml b/ide/utils/configwin_keys.ml index e1d7f33bb..9f44e5c6b 100644 --- a/ide/utils/configwin_keys.ml +++ b/ide/utils/configwin_keys.ml @@ -25,7 +25,7 @@ (** Key codes - Ce fichier provient de X11/keysymdef.h + Ce fichier provient de X11/keysymdef.h les noms des symboles deviennent : XK_ -> xk_ Thanks to Fabrice Le Fessant. @@ -1334,11 +1334,11 @@ let xk_Thai_khokhai = 0xda2 let xk_Thai_khokhuat = 0xda3 let xk_Thai_khokhwai = 0xda4 let xk_Thai_khokhon = 0xda5 -let xk_Thai_khorakhang = 0xda6 -let xk_Thai_ngongu = 0xda7 -let xk_Thai_chochan = 0xda8 -let xk_Thai_choching = 0xda9 -let xk_Thai_chochang = 0xdaa +let xk_Thai_khorakhang = 0xda6 +let xk_Thai_ngongu = 0xda7 +let xk_Thai_chochan = 0xda8 +let xk_Thai_choching = 0xda9 +let xk_Thai_chochang = 0xdaa let xk_Thai_soso = 0xdab let xk_Thai_chochoe = 0xdac let xk_Thai_yoying = 0xdad @@ -1380,39 +1380,39 @@ let xk_Thai_saraa = 0xdd0 let xk_Thai_maihanakat = 0xdd1 let xk_Thai_saraaa = 0xdd2 let xk_Thai_saraam = 0xdd3 -let xk_Thai_sarai = 0xdd4 -let xk_Thai_saraii = 0xdd5 -let xk_Thai_saraue = 0xdd6 -let xk_Thai_sarauee = 0xdd7 -let xk_Thai_sarau = 0xdd8 -let xk_Thai_sarauu = 0xdd9 +let xk_Thai_sarai = 0xdd4 +let xk_Thai_saraii = 0xdd5 +let xk_Thai_saraue = 0xdd6 +let xk_Thai_sarauee = 0xdd7 +let xk_Thai_sarau = 0xdd8 +let xk_Thai_sarauu = 0xdd9 let xk_Thai_phinthu = 0xdda let xk_Thai_maihanakat_maitho = 0xdde let xk_Thai_baht = 0xddf -let xk_Thai_sarae = 0xde0 +let xk_Thai_sarae = 0xde0 let xk_Thai_saraae = 0xde1 let xk_Thai_sarao = 0xde2 -let xk_Thai_saraaimaimuan = 0xde3 -let xk_Thai_saraaimaimalai = 0xde4 +let xk_Thai_saraaimaimuan = 0xde3 +let xk_Thai_saraaimaimalai = 0xde4 let xk_Thai_lakkhangyao = 0xde5 let xk_Thai_maiyamok = 0xde6 let xk_Thai_maitaikhu = 0xde7 -let xk_Thai_maiek = 0xde8 +let xk_Thai_maiek = 0xde8 let xk_Thai_maitho = 0xde9 let xk_Thai_maitri = 0xdea let xk_Thai_maichattawa = 0xdeb let xk_Thai_thanthakhat = 0xdec let xk_Thai_nikhahit = 0xded -let xk_Thai_leksun = 0xdf0 -let xk_Thai_leknung = 0xdf1 -let xk_Thai_leksong = 0xdf2 +let xk_Thai_leksun = 0xdf0 +let xk_Thai_leknung = 0xdf1 +let xk_Thai_leksong = 0xdf2 let xk_Thai_leksam = 0xdf3 -let xk_Thai_leksi = 0xdf4 -let xk_Thai_lekha = 0xdf5 -let xk_Thai_lekhok = 0xdf6 -let xk_Thai_lekchet = 0xdf7 -let xk_Thai_lekpaet = 0xdf8 -let xk_Thai_lekkao = 0xdf9 +let xk_Thai_leksi = 0xdf4 +let xk_Thai_lekha = 0xdf5 +let xk_Thai_lekhok = 0xdf6 +let xk_Thai_lekchet = 0xdf7 +let xk_Thai_lekpaet = 0xdf8 +let xk_Thai_lekkao = 0xdf9 (* diff --git a/ide/utils/configwin_types.ml b/ide/utils/configwin_types.ml index 0def0b25d..bf2b74ee6 100644 --- a/ide/utils/configwin_types.ml +++ b/ide/utils/configwin_types.ml @@ -111,7 +111,7 @@ let modifiers_to_string m = ) ^ s) in iter m "" - + let value_to_key v = match v with Raw.String s -> string_to_key s @@ -233,7 +233,7 @@ type hotkey_param = { type modifiers_param = { md_label : string ; (** the label of the parameter *) - mutable md_value : Gdk.Tags.modifier list ; + mutable md_value : Gdk.Tags.modifier list ; (** The value, as a list of modifiers and a key code *) md_editable : bool ; (** indicates if the value can be changed *) md_f_apply : Gdk.Tags.modifier list -> unit ; @@ -241,7 +241,7 @@ type modifiers_param = { md_help : string option ; (** optional help string *) md_expand : bool ; (** expand or not *) md_allow : Gdk.Tags.modifier list - } + } let mk_custom_text_string_param (a : 'a string_param) : string string_param = diff --git a/ide/utils/editable_cells.ml b/ide/utils/editable_cells.ml index 5441f4abe..1ab107c77 100644 --- a/ide/utils/editable_cells.ml +++ b/ide/utils/editable_cells.ml @@ -1,21 +1,21 @@ open GTree open Gobject -let create l = +let create l = let hbox = GPack.hbox () in - let scw = GBin.scrolled_window - ~hpolicy:`AUTOMATIC - ~vpolicy:`AUTOMATIC + let scw = GBin.scrolled_window + ~hpolicy:`AUTOMATIC + ~vpolicy:`AUTOMATIC ~packing:(hbox#pack ~expand:true) () in let columns = new GTree.column_list in let command_col = columns#add Data.string in let coq_col = columns#add Data.string in let store = GTree.list_store columns - in + in (* populate the store *) - let _ = List.iter (fun (x,y) -> + let _ = List.iter (fun (x,y) -> let row = store#append () in store#set ~row ~column:command_col x; store#set ~row ~column:coq_col y) @@ -27,61 +27,61 @@ let create l = view#set_rules_hint true; let renderer_comm = GTree.cell_renderer_text [`EDITABLE true] in - ignore (renderer_comm#connect#edited - ~callback:(fun (path:Gtk.tree_path) (s:string) -> - store#set - ~row:(store#get_iter path) + ignore (renderer_comm#connect#edited + ~callback:(fun (path:Gtk.tree_path) (s:string) -> + store#set + ~row:(store#get_iter path) ~column:command_col s)); - let first = - GTree.view_column ~title:"Coq Command to try" - ~renderer:(renderer_comm,["text",command_col]) - () + let first = + GTree.view_column ~title:"Coq Command to try" + ~renderer:(renderer_comm,["text",command_col]) + () in ignore (view#append_column first); let renderer_coq = GTree.cell_renderer_text [`EDITABLE true] in ignore(renderer_coq#connect#edited - ~callback:(fun (path:Gtk.tree_path) (s:string) -> - store#set - ~row:(store#get_iter path) + ~callback:(fun (path:Gtk.tree_path) (s:string) -> + store#set + ~row:(store#get_iter path) ~column:coq_col s)); - let second = - GTree.view_column ~title:"Coq Command to insert" - ~renderer:(renderer_coq,["text",coq_col]) - () + let second = + GTree.view_column ~title:"Coq Command to insert" + ~renderer:(renderer_coq,["text",coq_col]) + () in ignore (view#append_column second); - let vbox = GPack.button_box `VERTICAL ~packing:hbox#pack ~layout:`SPREAD () + let vbox = GPack.button_box `VERTICAL ~packing:hbox#pack ~layout:`SPREAD () in let up = GButton.button ~stock:`GO_UP ~label:"Up" ~packing:(vbox#pack ~expand:true ~fill:false) () in - let down = GButton.button - ~stock:`GO_DOWN - ~label:"Down" - ~packing:(vbox#pack ~expand:true ~fill:false) () + let down = GButton.button + ~stock:`GO_DOWN + ~label:"Down" + ~packing:(vbox#pack ~expand:true ~fill:false) () in - let add = GButton.button ~stock:`ADD - ~label:"Add" - ~packing:(vbox#pack ~expand:true ~fill:false) - () + let add = GButton.button ~stock:`ADD + ~label:"Add" + ~packing:(vbox#pack ~expand:true ~fill:false) + () in - let remove = GButton.button ~stock:`REMOVE - ~label:"Remove" - ~packing:(vbox#pack ~expand:true ~fill:false) () + let remove = GButton.button ~stock:`REMOVE + ~label:"Remove" + ~packing:(vbox#pack ~expand:true ~fill:false) () in - ignore (add#connect#clicked - ~callback:(fun b -> + ignore (add#connect#clicked + ~callback:(fun b -> let n = store#append () in view#selection#select_iter n)); - ignore (remove#connect#clicked - ~callback:(fun b -> match view#selection#get_selected_rows with + ignore (remove#connect#clicked + ~callback:(fun b -> match view#selection#get_selected_rows with | [] -> () | path::_ -> let iter = store#get_iter path in ignore (store#remove iter); )); - ignore (up#connect#clicked - ~callback:(fun b -> - match view#selection#get_selected_rows with + ignore (up#connect#clicked + ~callback:(fun b -> + match view#selection#get_selected_rows with | [] -> () | path::_ -> let iter = store#get_iter path in @@ -89,9 +89,9 @@ let create l = let upiter = store#get_iter path in ignore (store#swap iter upiter); )); - ignore (down#connect#clicked - ~callback:(fun b -> - match view#selection#get_selected_rows with + ignore (down#connect#clicked + ~callback:(fun b -> + match view#selection#get_selected_rows with | [] -> () | path::_ -> let iter = store#get_iter path in @@ -100,13 +100,13 @@ let create l = ignore (store#swap iter upiter) with _ -> () )); - let get_data () = + let get_data () = let start_path = GtkTree.TreePath.from_string "0" in let start_iter = store#get_iter start_path in - let rec all acc = + let rec all acc = let new_acc = (store#get ~row:start_iter ~column:command_col, store#get ~row:start_iter ~column:coq_col)::acc - in + in if store#iter_next start_iter then all new_acc else List.rev new_acc in all [] in diff --git a/ide/utils/okey.mli b/ide/utils/okey.mli index c8d48389c..84ea4df44 100644 --- a/ide/utils/okey.mli +++ b/ide/utils/okey.mli @@ -23,7 +23,7 @@ (* *) (*********************************************************************************) -(** Okey interface. +(** Okey interface. Once the lib is compiled and installed, you can use it by referencing it with the [Okey] module. You must add [okey.cmo] or [okey.cmx] @@ -35,7 +35,7 @@ type modifier = Gdk.Tags.modifier (** Set the default modifier list. The first default value is [[]].*) val set_default_modifiers : modifier list -> unit -(** Set the default modifier mask. The first default value is +(** Set the default modifier mask. The first default value is [[`MOD2 ; `MOD3 ; `MOD4 ; `MOD5 ; `LOCK]]. The mask defines the modifiers not taken into account when looking for the handler of a key press event. @@ -48,67 +48,67 @@ val set_default_mask : modifier list -> unit @param remove when true, the previous handlers for the given key and modifier list are not kept. @param cond this function is a guard: the [callback] function is not called - if the [cond] function returns [false]. + if the [cond] function returns [false]. The default [cond] function always returns [true]. @param mods the list of modifiers. If not given, the default modifiers - are used. + are used. You can set the default modifiers with function {!Okey.set_default_modifiers}. @param mask the list of modifiers which must not be taken into account to trigger the given handler. [mods] and [mask] must not have common modifiers. If not given, the default mask - is used. + is used. You can set the default modifiers mask with function {!Okey.set_default_mask}. *) val add : < connect : < destroy : callback: (unit -> unit) -> GtkSignal.id; .. >; - event : GObj.event_ops; get_oid : int; .. > -> - ?cond: (unit -> bool) -> - ?mods: modifier list -> - ?mask: modifier list -> - Gdk.keysym -> - (unit -> unit) -> + event : GObj.event_ops; get_oid : int; .. > -> + ?cond: (unit -> bool) -> + ?mods: modifier list -> + ?mask: modifier list -> + Gdk.keysym -> + (unit -> unit) -> unit (** It calls {!Okey.add} for each given key.*) -val add_list : +val add_list : < connect : < destroy : callback: (unit -> unit) -> GtkSignal.id; .. >; - event : GObj.event_ops; get_oid : int; .. > -> - ?cond: (unit -> bool) -> - ?mods: modifier list -> - ?mask: modifier list -> - Gdk.keysym list -> - (unit -> unit) -> + event : GObj.event_ops; get_oid : int; .. > -> + ?cond: (unit -> bool) -> + ?mods: modifier list -> + ?mask: modifier list -> + Gdk.keysym list -> + (unit -> unit) -> unit - + (** Like {!Okey.add} but the previous handlers for the given modifiers and key are not kept.*) val set : < connect : < destroy : callback: (unit -> unit) -> GtkSignal.id; .. >; - event : GObj.event_ops; get_oid : int; .. > -> - ?cond: (unit -> bool) -> - ?mods: modifier list -> - ?mask: modifier list -> - Gdk.keysym -> - (unit -> unit) -> + event : GObj.event_ops; get_oid : int; .. > -> + ?cond: (unit -> bool) -> + ?mods: modifier list -> + ?mask: modifier list -> + Gdk.keysym -> + (unit -> unit) -> unit (** It calls {!Okey.set} for each given key.*) -val set_list : +val set_list : < connect : < destroy : callback: (unit -> unit) -> GtkSignal.id; .. >; event : GObj.event_ops; get_oid : int; .. > -> - ?cond: (unit -> bool) -> - ?mods: modifier list -> - ?mask: modifier list -> - Gdk.keysym list -> - (unit -> unit) -> + ?cond: (unit -> bool) -> + ?mods: modifier list -> + ?mask: modifier list -> + Gdk.keysym list -> + (unit -> unit) -> unit (** Remove the handlers associated to the given widget. This is automatically done when a widget is destroyed but you can do it yourself. *) -val remove_widget : +val remove_widget : < connect : < destroy : callback: (unit -> unit) -> GtkSignal.id; .. >; event : GObj.event_ops; get_oid : int; .. > -> unit -> -- cgit v1.2.3