diff options
| -rw-r--r-- | ide/coqide.ml | 51 | ||||
| -rw-r--r-- | ide/coqide_ui.ml | 7 | ||||
| -rw-r--r-- | ide/preferences.ml | 49 | ||||
| -rw-r--r-- | ide/preferences.mli | 12 |
4 files changed, 56 insertions, 63 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 91e3ca04c..358302d3c 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -2459,6 +2459,16 @@ let main files = ~callback:(fun _ -> session_notebook#previous_page ()); GAction.add_action "Next tab" ~label:"_Next tab" ~accel:("<SHIFT>Right") ~stock:`GO_FORWARD ~callback:(fun _ -> session_notebook#next_page ()); + GAction.add_toggle_action "Show Toolbar" ~label:"Show _Toolbar" + ~active:(!current.show_toolbar) ~callback: + (fun _ -> !current.show_toolbar <- not !current.show_toolbar; + !refresh_toolbar_hook ()); + GAction.add_toggle_action "Show Query Pane" ~label:"Show _Query Pane" + ~callback:(fun _ -> let ccw = session_notebook#current_term.command in + if ccw#frame#misc#visible + then ccw#frame#misc#hide () + else ccw#frame#misc#show ()) + ~accel:"Escape"; ]; List.iter (fun (opts,name,label,key,dflt) -> @@ -2560,16 +2570,6 @@ let main files = ]; GAction.add_actions windows_actions [ GAction.add_action "Windows" ~label:"_Windows"; - GAction.add_toggle_action "Show/Hide Query Pane" ~label:"Show/Hide _Query Pane" - ~callback:(fun _ -> let ccw = session_notebook#current_term.command in - if ccw#frame#misc#visible - then ccw#frame#misc#hide () - else ccw#frame#misc#show ()) - ~accel:"Escape"; - GAction.add_toggle_action "Show/Hide Toolbar" ~label:"Show/Hide _Toolbar" - ~active:(!current.show_toolbar) ~callback: - (fun _ -> !current.show_toolbar <- not !current.show_toolbar; - !show_toolbar !current.show_toolbar); GAction.add_action "Detach View" ~label:"Detach _View" ~callback:(fun _ -> do_if_not_computing "detach view" (function {script=v;analyzed_view=av} -> @@ -2634,9 +2634,6 @@ let main files = let toolbar = new GObj.widget tbar in vbox#pack toolbar; - show_toolbar := - (fun b -> if b then toolbar#misc#show () else toolbar#misc#hide ()); - ignore (w#event#connect#delete ~callback:(fun _ -> quit_f (); true)); (* The vertical Separator between Scripts and Goals *) @@ -2799,9 +2796,14 @@ let main files = (* Progress Bar *) lower_hbox#pack pbar#coerce; pbar#set_text "CoqIde started"; - (* XXX *) - change_font := - (fun fd -> + + (* Initializing hooks *) + + refresh_toolbar_hook := + (fun () -> if !current.show_toolbar then toolbar#misc#show () else toolbar#misc#hide ()); + refresh_font_hook := + (fun () -> + let fd = !current.text_font in List.iter (fun {script=view; proof_view=prf_v; message_view=msg_v} -> view#misc#modify_font fd; @@ -2810,8 +2812,9 @@ let main files = ) session_notebook#pages; ); - change_background_color := - (fun clr -> + refresh_background_color_hook := + (fun () -> + let clr = Tags.color_of_string !current.background_color in List.iter (fun {script=view; proof_view=prf_v; message_view=msg_v} -> view#misc#modify_base [`NORMAL, `COLOR clr]; @@ -2820,6 +2823,12 @@ let main files = ) session_notebook#pages; ); + resize_window_hook := (fun () -> + w#resize + ~width:!current.window_width + ~height:!current.window_height); + refresh_tabs_hook := update_notebook_pos; + let about_full_string = "\nCoq is developed by the Coq Development Team\ \n(INRIA - CNRS - LIX - LRI - PPS)\ @@ -2890,10 +2899,6 @@ let main files = Tags.set_processed_color (Tags.color_of_string !current.processed_color); (* End of color configuration *) - resize_window := (fun () -> - w#resize - ~width:!current.window_width - ~height:!current.window_height); ignore(nb#connect#switch_page ~callback: (fun i -> @@ -2917,7 +2922,7 @@ let main files = session_notebook#goto_page index; end; initial_about session_notebook#current_term.proof_view#buffer; - !show_toolbar !current.show_toolbar; + !refresh_toolbar_hook (); session_notebook#current_term.script#misc#grab_focus ();; (* This function check every half of second if GeoProof has send diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index a29197486..eaf1e9348 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -59,7 +59,10 @@ let init () = <menu name='View' action='View'> <menuitem action='Previous tab' /> <menuitem action='Next tab' /> - <separator /> + <separator/> + <menuitem action='Show Toolbar' /> + <menuitem action='Show Query Pane' /> + <separator/> <menuitem action='Display implicit arguments' /> <menuitem action='Display coercions' /> <menuitem action='Display raw matching expressions' /> @@ -120,8 +123,6 @@ let init () = <menuitem action='Make makefile' /> </menu> <menu action='Windows'> - <menuitem action='Show/Hide Query Pane' /> - <menuitem action='Show/Hide Toolbar' /> <menuitem action='Detach View' /> </menu> <menu name='Help' action='Help'> diff --git a/ide/preferences.ml b/ide/preferences.ml index 180daa38d..eb63b1489 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -10,7 +10,6 @@ open Configwin open Printf let pref_file = Filename.concat Minilib.xdg_config_home "coqiderc" - let accel_file = Filename.concat Minilib.xdg_config_home "coqide.keys" let get_config_file name = @@ -66,6 +65,17 @@ let inputenc_of_string s = else if s = "LOCALE" then Elocale else Emanual s) + +(** Hooks *) + +let refresh_font_hook = ref (fun () -> ()) +let refresh_background_color_hook = ref (fun () -> ()) +let refresh_toolbar_hook = ref (fun () -> ()) +let auto_complete_hook = ref (fun x -> ()) +let contextual_menus_on_goal_hook = ref (fun x -> ()) +let resize_window_hook = ref (fun () -> ()) +let refresh_tabs_hook = ref (fun () -> ()) + type pref = { mutable cmd_coqtop : string option; @@ -114,7 +124,6 @@ type pref = *) mutable auto_complete : bool; mutable stop_before : bool; - mutable lax_syntax : bool; mutable vertical_tabs : bool; mutable opposite_tabs : bool; @@ -179,7 +188,6 @@ let (current:pref ref) = *) auto_complete = false; stop_before = true; - lax_syntax = true; vertical_tabs = false; opposite_tabs = false; @@ -189,19 +197,6 @@ let (current:pref ref) = } - -let change_font = ref (fun f -> ()) - -let change_background_color = ref (fun clr -> ()) - -let show_toolbar = ref (fun x -> ()) - -let auto_complete = ref (fun x -> ()) - -let contextual_menus_on_goal = ref (fun x -> ()) - -let resize_window = ref (fun () -> ()) - let save_pref () = if not (Sys.file_exists Minilib.xdg_config_home) then Unix.mkdir Minilib.xdg_config_home 0o700; @@ -251,7 +246,6 @@ let save_pref () = add "query_window_width" [string_of_int p.query_window_width] ++ add "auto_complete" [string_of_bool p.auto_complete] ++ add "stop_before" [string_of_bool p.stop_before] ++ - add "lax_syntax" [string_of_bool p.lax_syntax] ++ add "vertical_tabs" [string_of_bool p.vertical_tabs] ++ add "opposite_tabs" [string_of_bool p.opposite_tabs] ++ add "background_color" [p.background_color] ++ @@ -324,7 +318,6 @@ let load_pref () = set_int "query_window_height" (fun v -> np.query_window_height <- v); set_bool "auto_complete" (fun v -> np.auto_complete <- v); set_bool "stop_before" (fun v -> np.stop_before <- v); - set_bool "lax_syntax" (fun v -> np.lax_syntax <- v); set_bool "vertical_tabs" (fun v -> np.vertical_tabs <- v); set_bool "opposite_tabs" (fun v -> np.opposite_tabs <- v); set_hd "background_color" (fun v -> np.background_color <- v); @@ -379,7 +372,7 @@ let configure ?(apply=(fun () -> ())) () = (* Format.printf "in config_font: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) - !change_font !current.text_font) + !refresh_font_hook ()) true in @@ -433,7 +426,7 @@ let configure ?(apply=(fun () -> ())) () = !current.background_color <- Tags.string_of_color background_button#color; !current.processing_color <- Tags.string_of_color processing_button#color; !current.processed_color <- Tags.string_of_color processed_button#color; - !change_background_color background_button#color; + !refresh_background_color_hook (); Tags.set_processing_color processing_button#color; Tags.set_processed_color processed_button#color in @@ -468,7 +461,7 @@ let configure ?(apply=(fun () -> ())) () = bool ~f:(fun s -> !current.auto_complete <- s; - !auto_complete s) + !auto_complete_hook s) "Auto Complete" !current.auto_complete in @@ -515,21 +508,15 @@ let configure ?(apply=(fun () -> ())) () = "Stop interpreting before the current point" !current.stop_before in - let lax_syntax = - bool - ~f:(fun s -> !current.lax_syntax <- s) - "Relax read-only constraint at end of command" !current.lax_syntax - in - let vertical_tabs = bool - ~f:(fun s -> !current.vertical_tabs <- s) + ~f:(fun s -> !current.vertical_tabs <- s; !refresh_tabs_hook ()) "Vertical tabs" !current.vertical_tabs in let opposite_tabs = bool - ~f:(fun s -> !current.opposite_tabs <- s) + ~f:(fun s -> !current.opposite_tabs <- s; !refresh_tabs_hook ()) "Tabs on opposite side" !current.opposite_tabs in @@ -668,11 +655,11 @@ let configure ?(apply=(fun () -> ())) () = bool ~f:(fun s -> !current.contextual_menus_on_goal <- s; - !contextual_menus_on_goal s) + !contextual_menus_on_goal_hook s) "Contextual menus on goal" !current.contextual_menus_on_goal in - let misc = [contextual_menus_on_goal;auto_complete;stop_before;lax_syntax; + let misc = [contextual_menus_on_goal;auto_complete;stop_before; vertical_tabs;opposite_tabs] in (* ATTENTION !!!!! L'onglet Fonts doit etre en premier pour eviter un bug !!!! diff --git a/ide/preferences.mli b/ide/preferences.mli index d862979fe..b680c6f02 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -57,7 +57,6 @@ type pref = *) mutable auto_complete : bool; mutable stop_before : bool; - mutable lax_syntax : bool; mutable vertical_tabs : bool; mutable opposite_tabs : bool; @@ -73,10 +72,11 @@ val current : pref ref val configure : ?apply:(unit -> unit) -> unit -> unit -val change_font : (Pango.font_description -> unit) ref -val change_background_color : (Gdk.color -> unit) ref -val show_toolbar : (bool -> unit) ref -val auto_complete : (bool -> unit) ref -val resize_window : (unit -> unit) ref +(* Hooks *) +val refresh_font_hook : (unit -> unit) ref +val refresh_background_color_hook : (unit -> unit) ref +val refresh_toolbar_hook : (unit -> unit) ref +val resize_window_hook : (unit -> unit) ref +val refresh_tabs_hook : (unit -> unit) ref val use_default_doc_url : string |