diff options
| -rw-r--r-- | ide/coqide.ml | 90 | ||||
| -rw-r--r-- | ide/preferences.ml | 115 | ||||
| -rw-r--r-- | ide/preferences.mli | 5 |
3 files changed, 61 insertions, 149 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index d90e9153c4..e8bdf5e0e9 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1087,52 +1087,35 @@ let build_ui () = ~stock:`ZOOM_FIT ~callback:(cb_on_current_term MiscMenu.zoom_fit); toggle_item "Show Toolbar" ~label:"Show _Toolbar" ~active:(show_toolbar#get) - ~callback:(fun _ -> - show_toolbar#set (not show_toolbar#get); - !refresh_toolbar_hook ()); + ~callback:(fun _ -> show_toolbar#set (not show_toolbar#get)); item "Query Pane" ~label:"_Query Pane" ~accel:"F1" ~callback:(cb_on_current_term MiscMenu.show_hide_query_pane) ]; toggle_items view_menu Coq.PrintOpt.bool_items; - menu navigation_menu [ - item "Navigation" ~label:"_Navigation"; - item "Forward" ~label:"_Forward" ~stock:`GO_DOWN ~callback:Nav.forward_one - ~tooltip:"Forward one command" - ~accel:(modifier_for_navigation#get ^"Down"); - item "Backward" ~label:"_Backward" ~stock:`GO_UP ~callback:Nav.backward_one - ~tooltip:"Backward one command" - ~accel:(modifier_for_navigation#get ^"Up"); - item "Go to" ~label:"_Go to" ~stock:`JUMP_TO ~callback:Nav.goto - ~tooltip:"Go to cursor" - ~accel:(modifier_for_navigation#get ^"Right"); - item "Start" ~label:"_Start" ~stock:`GOTO_TOP ~callback:Nav.restart - ~tooltip:"Restart coq" - ~accel:(modifier_for_navigation#get ^"Home"); - item "End" ~label:"_End" ~stock:`GOTO_BOTTOM ~callback:Nav.goto_end - ~tooltip:"Go to end" - ~accel:(modifier_for_navigation#get ^"End"); - item "Interrupt" ~label:"_Interrupt" ~stock:`STOP ~callback:Nav.interrupt - ~tooltip:"Interrupt computations" - ~accel:(modifier_for_navigation#get ^"Break"); -(* wait for this available in GtkSourceView ! - item "Hide" ~label:"_Hide" ~stock:`MISSING_IMAGE - ~callback:(fun _ -> let sess = notebook#current_term in - toggle_proof_visibility sess.buffer - sess.analyzed_view#get_insert) ~tooltip:"Hide proof" - ~accel:(prefs.modifier_for_navigation^"h");*) - item "Previous" ~label:"_Previous" ~stock:`GO_BACK - ~callback:Nav.previous_occ - ~tooltip:"Previous occurence" - ~accel:(modifier_for_navigation#get ^"less"); - item "Next" ~label:"_Next" ~stock:`GO_FORWARD ~callback:Nav.next_occ - ~tooltip:"Next occurence" - ~accel:(modifier_for_navigation#get ^"greater"); - item "Force" ~label:"_Force" ~stock:`EXECUTE ~callback:Nav.join_document - ~tooltip:"Fully check the document" - ~accel:(modifier_for_navigation#get ^"f"); - ]; + let navitem (text, label, stock, callback, tooltip, accel) = + let accel = modifier_for_navigation#get ^ accel in + item text ~label ~stock ~callback ~tooltip ~accel + in + menu navigation_menu begin + [ + (fun e -> item "Navigation" ~label:"_Navigation" e); + ] @ List.map navitem [ + ("Forward", "_Forward", `GO_DOWN, Nav.forward_one, "Forward one command", "Down"); + ("Backward", "_Backward", `GO_UP, Nav.backward_one, "Backward one command", "Up"); + ("Go to", "_Go to", `JUMP_TO, Nav.goto, "Go to cursor", "Right"); + ("Start", "_Start", `GOTO_TOP, Nav.restart, "Restart coq", "Home"); + ("End", "_End", `GOTO_BOTTOM, Nav.goto_end, "Go to end", "End"); + ("Interrupt", "_Interrupt", `STOP, Nav.interrupt, "Interrupt computations", "Break"); + (* wait for this available in GtkSourceView ! + ("Hide", "_Hide", `MISSING_IMAGE, + ~callback:(fun _ -> let sess = notebook#current_term in + toggle_proof_visibility sess.buffer sess.analyzed_view#get_insert), "Hide proof", "h"); *) + ("Previous", "_Previous", `GO_BACK, Nav.previous_occ, "Previous occurence", "less"); + ("Next", "_Next", `GO_FORWARD, Nav.next_occ, "Next occurence", "greater"); + ("Force", "_Force", `EXECUTE, Nav.join_document, "Fully check the document", "f"); + ] end; let tacitem s sc = item s ~label:("_"^s) @@ -1309,31 +1292,24 @@ let build_ui () = let _ = Glib.Timeout.add ~ms:300 ~callback in (* Initializing hooks *) - let refresh_toolbar () = - if show_toolbar#get - then toolbar#misc#show () - else toolbar#misc#hide () + let refresh_toolbar b = + if b then toolbar#misc#show () else toolbar#misc#hide () in - let refresh_style () = - let style = style_manager#style_scheme source_style#get in + let refresh_style style = + let style = style_manager#style_scheme style in let iter_session v = v.script#source_buffer#set_style_scheme style in List.iter iter_session notebook#pages in - let refresh_language () = - let lang = lang_manager#language source_language#get in + let refresh_language lang = + let lang = lang_manager#language lang in let iter_session v = v.script#source_buffer#set_language lang in List.iter iter_session notebook#pages in - let resize_window () = - w#resize ~width:window_width#get ~height:window_height#get - in - refresh_toolbar (); - refresh_toolbar_hook := refresh_toolbar; - refresh_style_hook := refresh_style; - refresh_language_hook := refresh_language; + refresh_toolbar show_toolbar#get; + let _ = show_toolbar#connect#changed refresh_toolbar in + let _ = source_style#connect#changed refresh_style in + let _ = source_language#connect#changed refresh_language in refresh_editor_hook := refresh_editor_prefs; - resize_window_hook := resize_window; - refresh_tabs_hook := refresh_notebook_pos; (* Color configuration *) Tags.Script.incomplete#set_property diff --git a/ide/preferences.ml b/ide/preferences.ml index f8149b4f66..ceae6d1be7 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -158,12 +158,7 @@ let inputenc_of_string s = (** Hooks *) -let refresh_style_hook = ref (fun () -> ()) -let refresh_language_hook = ref (fun () -> ()) let refresh_editor_hook = ref (fun () -> ()) -let refresh_toolbar_hook = ref (fun () -> ()) -let resize_window_hook = ref (fun () -> ()) -let refresh_tabs_hook = ref (fun () -> ()) (** New style preferences *) @@ -427,6 +422,12 @@ let load_pref () = let pstring name p = string ~f:p#set name p#get let pbool name p = bool ~f:p#set name p#get +let pmodifiers ?(all = false) name p = modifiers + ?allow:(if all then None else Some (str_to_mod_list modifiers_valid#get)) + ~f:(fun l -> p#set (mod_list_to_str l)) + ~help:"restart to apply" + name + (str_to_mod_list p#get) let configure ?(apply=(fun () -> ())) () = let cmd_coqtop = @@ -544,46 +545,22 @@ let configure ?(apply=(fun () -> ())) () = let config_editor = let label = "Editor configuration" in let box = GPack.vbox () in - let gen_button text active = - GButton.check_button ~label:text ~active ~packing:box#pack () in - let wrap = gen_button "Dynamic word wrap" dynamic_word_wrap#get in - let line = gen_button "Show line number" show_line_number#get in - let b_auto_indent = gen_button "Auto indentation" auto_indent#get in - let b_auto_complete = gen_button "Auto completion" auto_complete#get in - let b_show_spaces = gen_button "Show spaces" show_spaces#get in - let b_show_right_margin = gen_button "Show right margin" show_right_margin#get in - let b_show_progress_bar = gen_button "Show progress bar" show_progress_bar#get in - let b_spaces_instead_of_tabs = - gen_button "Insert spaces instead of tabs" - spaces_instead_of_tabs#get - in - let b_highlight_current_line = - gen_button "Highlight current line" - highlight_current_line#get - in - let b_nanoPG = gen_button "Emacs/PG keybindings (μPG mode)" nanoPG#get in -(* let lbox = GPack.hbox ~packing:box#pack () in *) -(* let _ = GMisc.label ~text:"Tab width" *) -(* ~xalign:0. *) -(* ~packing:(lbox#pack ~expand:true) () *) -(* in *) -(* let tab_width = GEdit.spin_button *) -(* ~digits:0 ~packing:lbox#pack () *) -(* in *) - let callback () = - dynamic_word_wrap#set wrap#active; - show_line_number#set line#active; - auto_indent#set b_auto_indent#active; - show_spaces#set b_show_spaces#active; - show_right_margin#set b_show_right_margin#active; - show_progress_bar#set b_show_progress_bar#active; - spaces_instead_of_tabs#set b_spaces_instead_of_tabs#active; - highlight_current_line#set b_highlight_current_line#active; - nanoPG#set b_nanoPG#active; - auto_complete#set b_auto_complete#active; -(* tab_length#set tab_width#value_as_int; *) - !refresh_editor_hook () + 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)) in + let () = button "Dynamic word wrap" dynamic_word_wrap in + let () = button "Show line number" show_line_number in + let () = button "Auto indentation" auto_indent in + let () = button "Auto completion" auto_complete in + let () = button "Show spaces" show_spaces in + let () = button "Show right margin" show_right_margin in + let () = button "Show progress bar" show_progress_bar in + let () = button "Insert spaces instead of tabs" spaces_instead_of_tabs in + let () = button "Highlight current line" highlight_current_line in + let () = button "Emacs/PG keybindings (μPG mode)" nanoPG in + let callback () = !refresh_editor_hook () in custom ~label box callback true in @@ -653,22 +630,14 @@ let configure ?(apply=(fun () -> ())) () = in let source_style = - let f s = - source_style#set s; - !refresh_style_hook () - in combo "Highlighting style:" - ~f ~new_allowed:false + ~f:source_style#set ~new_allowed:false style_manager#style_scheme_ids source_style#get in let source_language = - let f s = - source_language#set s; - !refresh_language_hook () - in combo "Language:" - ~f ~new_allowed:false + ~f:source_language#set ~new_allowed:false (List.filter (fun x -> Str.string_match (Str.regexp "^coq") x 0) lang_manager#language_ids) @@ -686,48 +655,20 @@ let configure ?(apply=(fun () -> ())) () = (string_of_project_behavior current.read_project) in let project_file_name = pstring "Default name for project file" project_file_name in - let help_string = - "restart to apply" - in - let the_valid_mod = str_to_mod_list modifiers_valid#get in let modifier_for_tactics = - modifiers - ~allow:the_valid_mod - ~f:(fun l -> modifier_for_tactics#set (mod_list_to_str l)) - ~help:help_string - "Modifiers for Tactics Menu" - (str_to_mod_list modifier_for_tactics#get) + pmodifiers "Modifiers for Tactics Menu" modifier_for_tactics in let modifier_for_templates = - modifiers - ~allow:the_valid_mod - ~f:(fun l -> modifier_for_templates#set (mod_list_to_str l)) - ~help:help_string - "Modifiers for Templates Menu" - (str_to_mod_list modifier_for_templates#get) + pmodifiers "Modifiers for Templates Menu" modifier_for_templates in let modifier_for_navigation = - modifiers - ~allow:the_valid_mod - ~f:(fun l -> modifier_for_navigation#set (mod_list_to_str l)) - ~help:help_string - "Modifiers for Navigation Menu" - (str_to_mod_list modifier_for_navigation#get) + pmodifiers "Modifiers for Navigation Menu" modifier_for_navigation in let modifier_for_display = - modifiers - ~allow:the_valid_mod - ~f:(fun l -> modifier_for_display#set (mod_list_to_str l)) - ~help:help_string - "Modifiers for View Menu" - (str_to_mod_list modifier_for_display#get) + pmodifiers "Modifiers for View Menu" modifier_for_display in let modifiers_valid = - modifiers - ~f:(fun l -> - modifiers_valid#set (mod_list_to_str l)) - "Allowed modifiers" - the_valid_mod + pmodifiers ~all:true "Allowed modifiers" modifiers_valid in let cmd_editor = let predefined = [ "emacs %s"; "vi %s"; "NOTEPAD %s" ] in diff --git a/ide/preferences.mli b/ide/preferences.mli index 0a83e609be..1da8b3157c 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -105,10 +105,5 @@ val configure : ?apply:(unit -> unit) -> unit -> unit (* Hooks *) val refresh_editor_hook : (unit -> unit) ref -val refresh_style_hook : (unit -> unit) ref -val refresh_language_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 |