diff options
-rw-r--r-- | ide/coqOps.ml | 3 | ||||
-rw-r--r-- | ide/coqide.ml | 17 | ||||
-rw-r--r-- | ide/preferences.ml | 117 | ||||
-rw-r--r-- | ide/preferences.mli | 2 | ||||
-rw-r--r-- | ide/session.ml | 16 | ||||
-rw-r--r-- | ide/session.mli | 1 | ||||
-rw-r--r-- | ide/tags.ml | 54 | ||||
-rw-r--r-- | ide/tags.mli | 19 | ||||
-rw-r--r-- | ide/wg_Command.ml | 11 | ||||
-rw-r--r-- | ide/wg_Command.mli | 1 | ||||
-rw-r--r-- | ide/wg_MessageView.ml | 12 | ||||
-rw-r--r-- | ide/wg_MessageView.mli | 1 | ||||
-rw-r--r-- | ide/wg_ProofView.ml | 4 | ||||
-rw-r--r-- | ide/wg_ScriptView.ml | 6 |
14 files changed, 87 insertions, 177 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 7f44ec2aa..b178ba4ae 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -160,12 +160,11 @@ object end let flags_to_color f = - let of_col c = `NAME (Tags.string_of_color c) in if List.mem `PROCESSING f then `NAME "blue" else if List.mem `ERROR f then `NAME "red" else if List.mem `UNSAFE f then `NAME "orange" else if List.mem `INCOMPLETE f then `NAME "gray" - else of_col (Tags.get_processed_color ()) + else `NAME Preferences.processed_color#get module Doc = Document diff --git a/ide/coqide.ml b/ide/coqide.ml index e8bdf5e0e..46d99913e 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -828,8 +828,6 @@ let refresh_editor_prefs () = else 0 in let fd = prefs.text_font in - let clr = Tags.color_of_string background_color#get - in let iter_session sn = (* Editor settings *) sn.script#set_wrap_mode wrap_mode; @@ -854,18 +852,6 @@ let refresh_editor_prefs () = sn.messages#modify_font fd; sn.command#refresh_font (); - (* Colors *) - Tags.set_processing_color (Tags.color_of_string processing_color#get); - Tags.set_processed_color (Tags.color_of_string processed_color#get); - Tags.set_error_color (Tags.color_of_string error_color#get); - Tags.set_error_fg_color (Tags.color_of_string error_fg_color#get); - sn.script#misc#modify_base [`NORMAL, `COLOR clr]; - sn.proof#misc#modify_base [`NORMAL, `COLOR clr]; - sn.messages#refresh_color (); - sn.command#refresh_color (); - sn.errpage#refresh_color (); - sn.jobpage#refresh_color (); - in List.iter iter_session notebook#pages @@ -1315,13 +1301,12 @@ let build_ui () = Tags.Script.incomplete#set_property (`BACKGROUND_STIPPLE (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02")); - Tags.Script.incomplete#set_property - (`BACKGROUND_GDK (Tags.get_processed_color ())); (* Showtime ! *) w#show () + (** {2 Coqide main function } *) let make_file_buffer f = diff --git a/ide/preferences.ml b/ide/preferences.ml index ceae6d1be..74ca6ca83 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -57,6 +57,8 @@ object (self) method connect = new preference_signals ~changed method get = data method set (n : 'a) = data <- n; changed#call n + method reset () = self#set default + method default = default end (** Useful marshallers *) @@ -269,19 +271,35 @@ let opposite_tabs = new preference ~name:["opposite_tabs"] ~init:false ~repr:Repr.(bool) let background_color = - new preference ~name:["background_color"] ~init:Tags.default_color ~repr:Repr.(string) + 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)) + +let attach_fg (pref : string preference) (tag : GText.tag) = + pref#connect#changed (fun c -> tag#set_property (`FOREGROUND c)) let processing_color = - new preference ~name:["processing_color"] ~init:Tags.default_processing_color ~repr:Repr.(string) + new preference ~name:["processing_color"] ~init:"light blue" ~repr:Repr.(string) + +let _ = attach_bg processing_color Tags.Script.to_process +let _ = attach_bg processing_color Tags.Script.incomplete let processed_color = - new preference ~name:["processed_color"] ~init:Tags.default_processed_color ~repr:Repr.(string) + new preference ~name:["processed_color"] ~init:"light green" ~repr:Repr.(string) + +let _ = attach_bg processed_color Tags.Script.processed +let _ = attach_bg processed_color Tags.Proof.highlight let error_color = - new preference ~name:["error_color"] ~init:Tags.default_error_color ~repr:Repr.(string) + new preference ~name:["error_color"] ~init:"#FFCCCC" ~repr:Repr.(string) + +let _ = attach_bg error_color Tags.Script.error_bg let error_fg_color = - new preference ~name:["error_fg_color"] ~init:Tags.default_error_fg_color ~repr:Repr.(string) + new preference ~name:["error_fg_color"] ~init:"red" ~repr:Repr.(string) + +let _ = attach_fg error_fg_color Tags.Script.error let dynamic_word_wrap = new preference ~name:["dynamic_word_wrap"] ~init:false ~repr:Repr.(bool) @@ -470,75 +488,38 @@ let configure ?(apply=(fun () -> ())) () = ~border_width:2 ~packing:(box#pack ~expand:true) () in - let background_label = GMisc.label - ~text:"Background color" - ~packing:(table#attach ~expand:`X ~left:0 ~top:0) () - in - let processed_label = GMisc.label - ~text:"Background color of processed text" - ~packing:(table#attach ~expand:`X ~left:0 ~top:1) () - in - let processing_label = GMisc.label - ~text:"Background color of text being processed" - ~packing:(table#attach ~expand:`X ~left:0 ~top:2) () - in - let error_label = GMisc.label - ~text:"Background color of errors" - ~packing:(table#attach ~expand:`X ~left:0 ~top:3) () - in - let error_fg_label = GMisc.label - ~text:"Foreground color of errors" - ~packing:(table#attach ~expand:`X ~left:0 ~top:4) () - in - let () = background_label#set_xalign 0. in - let () = processed_label#set_xalign 0. in - let () = processing_label#set_xalign 0. in - let () = error_label#set_xalign 0. in - let () = error_fg_label#set_xalign 0. in - let background_button = GButton.color_button - ~color:(Tags.color_of_string (background_color#get)) - ~packing:(table#attach ~left:1 ~top:0) () - in - let processed_button = GButton.color_button - ~color:(Tags.get_processed_color ()) - ~packing:(table#attach ~left:1 ~top:1) () - in - let processing_button = GButton.color_button - ~color:(Tags.get_processing_color ()) - ~packing:(table#attach ~left:1 ~top:2) () - in - let error_button = GButton.color_button - ~color:(Tags.get_error_color ()) - ~packing:(table#attach ~left:1 ~top:3) () - in - let error_fg_button = GButton.color_button - ~color:(Tags.get_error_fg_color ()) - ~packing:(table#attach ~left:1 ~top:4) () - in let reset_button = GButton.button ~label:"Reset" ~packing:box#pack () in - let reset_cb () = - background_button#set_color Tags.(color_of_string default_color); - processing_button#set_color Tags.(color_of_string default_processing_color); - processed_button#set_color Tags.(color_of_string default_processed_color); - error_button#set_color Tags.(color_of_string default_error_color); + let iter i (text, pref) = + let label = GMisc.label + ~text ~packing:(table#attach ~expand:`X ~left:0 ~top:i) () + in + let () = label#set_xalign 0. in + let button = GButton.color_button + ~color:(Tags.color_of_string pref#get) + ~packing:(table#attach ~left:1 ~top:i) () + in + let _ = button#connect#color_set begin fun () -> + pref#set (Tags.string_of_color button#color) + end in + let reset _ = + pref#reset (); + button#set_color Tags.(color_of_string pref#get) + in + let _ = reset_button#connect#clicked ~callback:reset in + () in - let _ = reset_button#connect#clicked ~callback:reset_cb in + let () = Util.List.iteri iter [ + ("Background color", background_color); + ("Background color of processed text", processed_color); + ("Background color of text being processed", processing_color); + ("Background color of errors", error_color); + ("Foreground color of errors", error_fg_color); + ] in let label = "Color configuration" in - let callback () = - background_color#set (Tags.string_of_color background_button#color); - processing_color#set (Tags.string_of_color processing_button#color); - processed_color#set (Tags.string_of_color processed_button#color); - error_color#set (Tags.string_of_color error_button#color); - error_fg_color#set (Tags.string_of_color error_fg_button#color); - !refresh_editor_hook (); - Tags.set_processing_color processing_button#color; - Tags.set_processed_color processed_button#color; - Tags.set_error_color error_button#color; - Tags.set_error_fg_color error_fg_button#color - in + let callback () = () in custom ~label box callback true in diff --git a/ide/preferences.mli b/ide/preferences.mli index 1da8b3157..48c2a6410 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -29,6 +29,8 @@ object method connect : 'a preference_signals method get : 'a method set : 'a -> unit + method reset : unit -> unit + method default : 'a end val cmd_coqtop : string option preference diff --git a/ide/session.ml b/ide/session.ml index 0b26c1f65..ceeb0abca 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -18,7 +18,6 @@ class type ['a] page = inherit GObj.widget method update : 'a -> unit method on_update : callback:('a -> unit) -> unit - method refresh_color : unit -> unit end class type control = @@ -254,10 +253,9 @@ let make_table_widget ?sort cd cb = ~model:store ~packing:frame#add () in let () = data#set_headers_visible true in let () = data#set_headers_clickable true in - let refresh () = - let clr = Tags.color_of_string background_color#get in - data#misc#modify_base [`NORMAL, `COLOR clr] - 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 mk_rend c = GTree.cell_renderer_text [], ["text",c] in let cols = List.map2 (fun (_,c) (_,n,v) -> @@ -285,10 +283,10 @@ let make_table_widget ?sort cd cb = data#connect#row_activated ~callback:(fun tp vc -> cb columns store tp vc) ); let () = match sort with None -> () | Some (i, t) -> store#set_sort_column_id i t in - frame, (fun f -> f columns store), refresh + frame, (fun f -> f columns store) let create_errpage (script : Wg_ScriptView.script_view) : errpage = - let table, access, refresh = + let table, access = make_table_widget ~sort:(0, `ASCENDING) [`Int,"Line",true; `String,"Error message",true] (fun columns store tp vc -> @@ -320,11 +318,10 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage = errs end method on_update ~callback:cb = callback := cb - method refresh_color () = refresh () end let create_jobpage coqtop coqops : jobpage = - let table, access, refresh = + let table, access = make_table_widget ~sort:(0, `ASCENDING) [`String,"Worker",true; `String,"Job name",true] (fun columns store tp vc -> @@ -360,7 +357,6 @@ let create_jobpage coqtop coqops : jobpage = jobs end method on_update ~callback:cb = callback := cb - method refresh_color () = refresh () end let create_proof () = diff --git a/ide/session.mli b/ide/session.mli index 52e557218..3a6b45858 100644 --- a/ide/session.mli +++ b/ide/session.mli @@ -14,7 +14,6 @@ class type ['a] page = inherit GObj.widget method update : 'a -> unit method on_update : callback:('a -> unit) -> unit - method refresh_color : unit -> unit end class type control = diff --git a/ide/tags.ml b/ide/tags.ml index c9b57af4c..09b562530 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -13,28 +13,15 @@ let make_tag (tt:GText.tag_table) ~name prop = tt#add new_tag#as_tag; new_tag -(* These work fine for colorblind people too *) -let default_processed_color = "light green" -let default_processing_color = "light blue" -let default_error_color = "#FFCCCC" -let default_error_fg_color = "red" -let default_color = "cornsilk" - -let processed_color = ref default_processed_color -let processing_color = ref default_processing_color -let error_color = ref default_error_color -let error_fg_color = ref default_error_fg_color - module Script = struct let table = GText.tag_table () let comment = make_tag table ~name:"comment" [] - let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE ; `FOREGROUND !error_fg_color] - let error_bg = make_tag table ~name:"error_bg" [`BACKGROUND !error_color] - let to_process = make_tag table ~name:"to_process" [`BACKGROUND !processing_color] - let processed = make_tag table ~name:"processed" [`BACKGROUND !processed_color] + let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE] + let error_bg = make_tag table ~name:"error_bg" [] + let to_process = make_tag table ~name:"to_process" [] + let processed = make_tag table ~name:"processed" [] let incomplete = make_tag table ~name:"incomplete" [ - `BACKGROUND !processing_color; `BACKGROUND_STIPPLE_SET true; ] let unjustified = make_tag table ~name:"unjustified" [`BACKGROUND "gold"] @@ -56,7 +43,7 @@ end module Proof = struct let table = GText.tag_table () - let highlight = make_tag table ~name:"highlight" [`BACKGROUND !processed_color] + let highlight = make_tag table ~name:"highlight" [] let hypothesis = make_tag table ~name:"hypothesis" [] let goal = make_tag table ~name:"goal" [] end @@ -77,34 +64,3 @@ let string_of_color clr = let color_of_string s = let colormap = Gdk.Color.get_system_colormap () in Gdk.Color.alloc ~colormap (`NAME s) - -let get_processed_color () = color_of_string !processed_color - -let set_processed_color clr = - let s = string_of_color clr in - processed_color := s; - Script.processed#set_property (`BACKGROUND s); - Proof.highlight#set_property (`BACKGROUND s) - -let get_processing_color () = color_of_string !processing_color - -let set_processing_color clr = - let s = string_of_color clr in - processing_color := s; - Script.incomplete#set_property (`BACKGROUND s); - Script.to_process#set_property (`BACKGROUND s) - -let get_error_color () = color_of_string !error_color - -let set_error_color clr = - let s = string_of_color clr in - error_color := s; - Script.error_bg#set_property (`BACKGROUND s) - -let get_error_fg_color () = color_of_string !error_fg_color - -let set_error_fg_color clr = - let s = string_of_color clr in - error_fg_color := s; - Script.error#set_property (`FOREGROUND s) - diff --git a/ide/tags.mli b/ide/tags.mli index 14cfd0dbf..6418d1b2e 100644 --- a/ide/tags.mli +++ b/ide/tags.mli @@ -41,22 +41,3 @@ end val string_of_color : Gdk.color -> string val color_of_string : string -> Gdk.color - -val get_processed_color : unit -> Gdk.color -val set_processed_color : Gdk.color -> unit - -val get_processing_color : unit -> Gdk.color -val set_processing_color : Gdk.color -> unit - -val get_error_color : unit -> Gdk.color -val set_error_color : Gdk.color -> unit - -val get_error_fg_color : unit -> Gdk.color -val set_error_fg_color : Gdk.color -> unit - -val default_processed_color : string -val default_processing_color : string -val default_error_color : string -val default_error_fg_color : string -val default_color : string - diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index bf25ddfa1..bfd37ea0e 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -86,8 +86,9 @@ object(self) let result = GText.view ~packing:r_bin#add () in views <- (frame#coerce, result, combo#entry) :: views; result#misc#modify_font current.text_font; - let clr = Tags.color_of_string background_color#get in - result#misc#modify_base [`NORMAL, `COLOR clr]; + 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 result#misc#set_can_focus true; (* false causes problems for selection *) result#set_editable false; let callback () = @@ -149,8 +150,8 @@ object(self) let iter (_,view,_) = view#misc#modify_font current.text_font in List.iter iter views - method refresh_color () = - let clr = Tags.color_of_string background_color#get in + method private refresh_color clr = + let clr = Tags.color_of_string clr in let iter (_,view,_) = view#misc#modify_base [`NORMAL, `COLOR clr] in List.iter iter views @@ -158,6 +159,8 @@ 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 + 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) else false diff --git a/ide/wg_Command.mli b/ide/wg_Command.mli index 91a8f26ca..c559ebef3 100644 --- a/ide/wg_Command.mli +++ b/ide/wg_Command.mli @@ -11,7 +11,6 @@ class command_window : string -> Coq.coqtop -> method new_query : ?command:string -> ?term:string -> unit -> unit method pack_in : (GObj.widget -> unit) -> unit method refresh_font : unit -> unit - method refresh_color : unit -> unit method show : unit method hide : unit method visible : bool diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 3fff01945..7b7f0fab1 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Preferences + class type message_view_signals = object inherit GObj.misc_signals @@ -33,7 +35,6 @@ class type message_view = method buffer : GText.buffer (** for more advanced text edition *) method modify_font : Pango.font_description -> unit - method refresh_color : unit -> unit end let message_view () : message_view = @@ -53,6 +54,10 @@ let message_view () : message_view = let default_clipboard = GData.clipboard Gdk.Atom.primary in let _ = buffer#add_selection_clipboard default_clipboard in let () = view#set_left_margin 2 in + view#misc#show (); + 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 object (self) inherit GObj.widget box#as_widget @@ -84,9 +89,4 @@ let message_view () : message_view = method modify_font fd = view#misc#modify_font fd - method refresh_color () = - let open Preferences in - let clr = Tags.color_of_string background_color#get in - view#misc#modify_base [`NORMAL, `COLOR clr] - end diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli index 23c94f404..4dcd7306b 100644 --- a/ide/wg_MessageView.mli +++ b/ide/wg_MessageView.mli @@ -25,7 +25,6 @@ class type message_view = method buffer : GText.buffer (** for more advanced text edition *) method modify_font : Pango.font_description -> unit - method refresh_color : unit -> unit end val message_view : unit -> message_view diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 69d460b01..e3a741394 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -7,6 +7,7 @@ (************************************************************************) open Util +open Preferences class type proof_view = object @@ -193,6 +194,9 @@ let proof_view () = let () = Gtk_parsing.fix_double_click view in 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 object inherit GObj.widget view#as_widget val mutable goals = None diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 8298d9954..3b3d9db4b 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Preferences + type insert_action = { ins_val : string; ins_off : int; @@ -456,6 +458,10 @@ object (self) if not proceed then GtkSignal.stop_emit () in 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 () end |