diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 31 | ||||
| -rw-r--r-- | ide/coqide_ui.ml | 13 | ||||
| -rw-r--r-- | ide/preferences.ml | 38 | ||||
| -rw-r--r-- | ide/preferences.mli | 1 |
4 files changed, 73 insertions, 10 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 2d1ba72f3..8697ca833 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -681,10 +681,6 @@ let doquery query sn = sn.messages#clear; Coq.try_grab sn.coqtop (sn.coqops#raw_coq_query query) ignore -let showproof () = - let query = "Show Proof." in - on_current_term (doquery query) - let otherquery command sn = let word = get_current_word sn in if word <> "" then @@ -696,10 +692,10 @@ let otherquery command = cb_on_current_term (otherquery command) let query command _ = if command = "Search" || command = "SearchAbout" then searchabout () - else if command = "Show Proof" - then showproof () else otherquery command () +let simplequery query = cb_on_current_term (doquery query) + end (** Misc *) @@ -868,12 +864,12 @@ let toggle_items menu_name l = in List.iter f l +let no_under = Util.String.map (fun x -> if x = '_' then '-' else x) + (** Create alphabetical menu items with elements in sub-items. [l] is a list of lists, one per initial letter *) let alpha_items menu_name item_name l = - let no_under = Util.String.map (fun x -> if x = '_' then '-' else x) - in let mk_item text = let text' = let last = String.length text - 1 in @@ -920,6 +916,24 @@ let template_item (text, offset, len, key) = in item name ~label ~callback:(cb_on_current_term callback) ~accel:(modifier^key) +(** Create menu items for pairs (query, shortcut key). + If the shortcut key is not in the range 'a'-'z','A'-'Z', it will be ignored. *) + +let user_queries_items menu_name item_name l modifier = + let valid_key k = Int.equal (CString.length k) 1 && Util.is_letter k.[0] in + let mk_item (query, key) = + let query' = + let last = CString.length query - 1 in + if query.[last] = '.' + then query + else query ^ "." + in + let callback = Query.simplequery query' in + let accel = if valid_key key then Some (modifier^key) else None in + item (item_name^" "^(no_under query)) ~label:query ?accel ~callback menu_name + in + List.iter mk_item l + let emit_to_focus window sgn = let focussed_widget = GtkWindow.Window.get_focus window#as_window in let obj = Gobject.unsafe_cast focussed_widget in @@ -1120,6 +1134,7 @@ let build_ui () = qitem "Print Assumptions" (Some "<Ctrl><Shift>N"); qitem "Show Proof" (Some "<Ctrl><Shift>R"); ]; + user_queries_items queries_menu "Query" user_queries#get "<Ctrl><Shift>"; menu tools_menu [ item "Tools" ~label:"_Tools"; diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index 65735240a..b45a9f12b 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -18,6 +18,15 @@ let list_items menu li = let () = List.iter (fun b -> Buffer.add_buffer res_buf (tactic_item b)) li in res_buf +let list_queries menu li = + let res_buf = Buffer.create 500 in + let query_item (q, _) = + let s = "<menuitem action='"^menu^" "^(no_under q)^"' />\n" in + Buffer.add_string res_buf s + in + let () = List.iter query_item li in + res_buf + let init () = let theui = Printf.sprintf "<ui> <menubar name='CoqIde MenuBar'> @@ -119,7 +128,8 @@ let init () = <menuitem action='About' /> <menuitem action='Locate' /> <menuitem action='Print Assumptions' /> - <menuitem action='Show Proof' /> + <separator /> + %s </menu> <menu name='Tools' action='Tools'> <menuitem action='Comment' /> @@ -163,5 +173,6 @@ let init () = (if Coq_config.gtk_platform <> `QUARTZ then "<menuitem action='Quit' />" else "") (Buffer.contents (list_items "Tactic" Coq_commands.tactics)) (Buffer.contents (list_items "Template" Coq_commands.commands)) + (Buffer.contents (list_queries "Query" Preferences.user_queries#get)) in ignore (ui_m#add_ui_from_string theui); diff --git a/ide/preferences.ml b/ide/preferences.ml index c4dc55972..b7fdc975c 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -144,6 +144,18 @@ object method into s = Some s end +let string_pair_list (sep : char) : (string * string) list repr = +object + val sep' = String.make 1 sep + method from = CList.map (fun (s1, s2) -> CString.concat sep' [s1; s2]) + method into l = + try + Some (CList.map (fun s -> + let split = CString.split sep s in + CList.nth split 0, CList.nth split 1) l) + with Failure _ -> None +end + let bool : bool repr = object method from s = [string_of_bool s] @@ -507,6 +519,9 @@ let highlight_current_line = let nanoPG = new preference ~name:["nanoPG"] ~init:false ~repr:Repr.(bool) +let user_queries = + new preference ~name:["user_queries"] ~init:[] ~repr:Repr.(string_pair_list '$') + class tag_button (box : Gtk.box Gtk.obj) = object (self) @@ -908,6 +923,25 @@ let configure ?(apply=(fun () -> ())) () = let misc = [contextual_menus_on_goal;stop_before;reset_on_tab_switch; vertical_tabs;opposite_tabs] in + let edit_user_query (q, k) = + let q = Configwin_ihm.edit_string "User query" q in + let k = Configwin_ihm.edit_string "Shortcut key" k in + q, k + in + + let user_queries = + list + ~f:user_queries#set + ~eq:(fun (q1, _) (q2, _) -> q1 = q2) + ~edit:edit_user_query + ~add:(fun () -> ["<user query>", "<shortcut key>"]) + ~titles:["User query"; "Shortcut key"] + "User queries" + (fun (q, s) -> [q; s]) + user_queries#get + + in + (* ATTENTION !!!!! L'onglet Fonts doit etre en premier pour eviter un bug !!!! (shame on Benjamin) *) let cmds = @@ -939,7 +973,9 @@ let configure ?(apply=(fun () -> ())) () = [modifiers_valid; modifier_for_tactics; modifier_for_templates; modifier_for_display; modifier_for_navigation]); Section("Misc", Some `ADD, - misc)] + misc); + Section("User queries", None, + [user_queries])] in (* Format.printf "before edit: current.text_font = %s@." (Pango.Font.to_string current.text_font); diff --git a/ide/preferences.mli b/ide/preferences.mli index 1733091a5..ebcff2080 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -95,6 +95,7 @@ val spaces_instead_of_tabs : bool preference val tab_length : int preference val highlight_current_line : bool preference val nanoPG : bool preference +val user_queries : (string * string) list preference val save_pref : unit -> unit val load_pref : unit -> unit |