From 6cc27d2ca57a5d2fedfa52d8b44c37c60ccb6988 Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Fri, 19 Jun 2015 12:53:51 +0200 Subject: Add a [Show Proof.] query to CoqIDE. --- ide/coqide.ml | 14 ++++++++++++-- ide/coqide_ui.ml | 1 + 2 files changed, 13 insertions(+), 2 deletions(-) (limited to 'ide') diff --git a/ide/coqide.ml b/ide/coqide.ml index 758a5a4c99..2d1ba72f3b 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -677,18 +677,27 @@ let searchabout sn = let searchabout () = on_current_term searchabout +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 let query = command ^ " " ^ word ^ "." in - sn.messages#clear; - Coq.try_grab sn.coqtop (sn.coqops#raw_coq_query query) ignore + doquery query sn 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 () end @@ -1109,6 +1118,7 @@ let build_ui () = qitem "About" (Some "A"); qitem "Locate" (Some "L"); qitem "Print Assumptions" (Some "N"); + qitem "Show Proof" (Some "R"); ]; menu tools_menu [ diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index edfe28b261..65735240aa 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -119,6 +119,7 @@ let init () = + -- cgit v1.2.3 From 5874843ea8e1ca82f8b1b646022582309b7fe24c Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Thu, 2 Jun 2016 11:29:43 +0200 Subject: Add user-created queries to CoqIDE. --- ide/coqide.ml | 31 +++++++++++++++++++++++-------- ide/coqide_ui.ml | 13 ++++++++++++- ide/preferences.ml | 38 +++++++++++++++++++++++++++++++++++++- ide/preferences.mli | 1 + 4 files changed, 73 insertions(+), 10 deletions(-) (limited to 'ide') diff --git a/ide/coqide.ml b/ide/coqide.ml index 2d1ba72f3b..8697ca8333 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 "N"); qitem "Show Proof" (Some "R"); ]; + user_queries_items queries_menu "Query" user_queries#get ""; menu tools_menu [ item "Tools" ~label:"_Tools"; diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index 65735240aa..b45a9f12b8 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 = "\n" in + Buffer.add_string res_buf s + in + let () = List.iter query_item li in + res_buf + let init () = let theui = Printf.sprintf " @@ -119,7 +128,8 @@ let init () = - + + %s @@ -163,5 +173,6 @@ let init () = (if Coq_config.gtk_platform <> `QUARTZ then "" 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 c4dc55972b..b7fdc975c2 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 () -> ["", ""]) + ~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 1733091a58..ebcff20808 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 -- cgit v1.2.3 From 2911de377786ad525dd9407968dae7c1973d7190 Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Tue, 7 Jul 2015 14:04:09 +0200 Subject: Slightly better interface to edit queries. --- ide/preferences.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'ide') diff --git a/ide/preferences.ml b/ide/preferences.ml index b7fdc975c2..b39a1106c2 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -924,8 +924,13 @@ let configure ?(apply=(fun () -> ())) () = 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 + let input_string l s v = + match GToolbox.input_string ~title:l ~text:s v with + | None -> s + | Some s -> s + in + let q = input_string "User query" q "Your query" in + let k = input_string "Shortcut key" k "Shortcut (a single letter)" in q, k in -- cgit v1.2.3 From abd469790c2e144f693e1b21c5cdc03aee178e6d Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Thu, 2 Jun 2016 11:34:10 +0200 Subject: Merge the user queries tab with the shortcut tab. --- ide/coqide.ml | 1 - ide/preferences.ml | 7 +++---- 2 files changed, 3 insertions(+), 5 deletions(-) (limited to 'ide') diff --git a/ide/coqide.ml b/ide/coqide.ml index 8697ca8333..d4f47b15e5 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1132,7 +1132,6 @@ let build_ui () = qitem "About" (Some "A"); qitem "Locate" (Some "L"); qitem "Print Assumptions" (Some "N"); - qitem "Show Proof" (Some "R"); ]; user_queries_items queries_menu "Query" user_queries#get ""; diff --git a/ide/preferences.ml b/ide/preferences.ml index b39a1106c2..6bb19c6389 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -976,11 +976,10 @@ let configure ?(apply=(fun () -> ())) () = [automatic_tactics]); Section("Shortcuts", Some `PREFERENCES, [modifiers_valid; modifier_for_tactics; - modifier_for_templates; modifier_for_display; modifier_for_navigation]); + modifier_for_templates; modifier_for_display; modifier_for_navigation; + user_queries]); Section("Misc", Some `ADD, - misc); - Section("User queries", None, - [user_queries])] + misc)] in (* Format.printf "before edit: current.text_font = %s@." (Pango.Font.to_string current.text_font); -- cgit v1.2.3 From c6d5f9c39b3e12f58745c22eade90d34548b6283 Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Thu, 2 Jun 2016 11:40:33 +0200 Subject: Add an option to configure the modifier for Queries. --- ide/coqide.ml | 24 ++++++++++++++---------- ide/preferences.ml | 8 +++++++- ide/preferences.mli | 1 + 3 files changed, 22 insertions(+), 11 deletions(-) (limited to 'ide') diff --git a/ide/coqide.ml b/ide/coqide.ml index d4f47b15e5..8b164d234c 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -919,7 +919,7 @@ let template_item (text, offset, len, 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 user_queries_items menu_name item_name l = let valid_key k = Int.equal (CString.length k) 1 && Util.is_letter k.[0] in let mk_item (query, key) = let query' = @@ -929,7 +929,7 @@ let user_queries_items menu_name item_name l modifier = else query ^ "." in let callback = Query.simplequery query' in - let accel = if valid_key key then Some (modifier^key) else None in + let accel = if valid_key key then Some (modifier_for_queries#get^key) else None in item (item_name^" "^(no_under query)) ~label:query ?accel ~callback menu_name in List.iter mk_item l @@ -1123,17 +1123,21 @@ let build_ui () = ]; alpha_items templates_menu "Template" Coq_commands.commands; - let qitem s accel = item s ~label:("_"^s) ?accel ~callback:(Query.query s) in + let qitem s sc = + item s ~label:("_"^s) + ~accel:(modifier_for_queries#get^sc) + ~callback:(Query.query s) + in menu queries_menu [ item "Queries" ~label:"_Queries"; - qitem "Search" (Some "K"); - qitem "Check" (Some "C"); - qitem "Print" (Some "P"); - qitem "About" (Some "A"); - qitem "Locate" (Some "L"); - qitem "Print Assumptions" (Some "N"); + qitem "Search" "K"; + qitem "Check" "C"; + qitem "Print" "P"; + qitem "About" "A"; + qitem "Locate" "L"; + qitem "Print Assumptions" "N"; ]; - user_queries_items queries_menu "Query" user_queries#get ""; + user_queries_items queries_menu "Query" user_queries#get; menu tools_menu [ item "Tools" ~label:"_Tools"; diff --git a/ide/preferences.ml b/ide/preferences.ml index 6bb19c6389..f2945a5e07 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -315,6 +315,9 @@ let modifier_for_tactics = let modifier_for_display = new preference ~name:["modifier_for_display"] ~init:"" ~repr:Repr.(string) +let modifier_for_queries = + new preference ~name:["modifier_for_queries"] ~init:"" ~repr:Repr.(string) + let _ = attach_modifiers modifier_for_navigation "/Navigation/" let _ = attach_modifiers modifier_for_templates "/Templates/" let _ = attach_modifiers modifier_for_tactics "/Tactics/" @@ -852,6 +855,9 @@ let configure ?(apply=(fun () -> ())) () = let modifier_for_display = pmodifiers "Modifiers for View Menu" modifier_for_display in + let modifier_for_queries = + pmodifiers "Modifiers for Queries Menu" modifier_for_queries + in let modifiers_valid = pmodifiers ~all:true "Allowed modifiers" modifiers_valid in @@ -977,7 +983,7 @@ let configure ?(apply=(fun () -> ())) () = Section("Shortcuts", Some `PREFERENCES, [modifiers_valid; modifier_for_tactics; modifier_for_templates; modifier_for_display; modifier_for_navigation; - user_queries]); + modifier_for_queries; user_queries]); Section("Misc", Some `ADD, misc)] in diff --git a/ide/preferences.mli b/ide/preferences.mli index ebcff20808..426b0a328e 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -65,6 +65,7 @@ val modifier_for_navigation : string preference val modifier_for_templates : string preference val modifier_for_tactics : string preference val modifier_for_display : string preference +val modifier_for_queries : string preference val modifiers_valid : string preference val cmd_browse : string preference val cmd_editor : string preference -- cgit v1.2.3 From 93be8ebeb69df9b53122a90a15bfd3fe917aa38a Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Thu, 2 Jun 2016 12:06:33 +0200 Subject: Better sanitization of user queries in CoqIDE. --- ide/coqide.ml | 16 ++++------------ ide/preferences.ml | 26 ++++++++++++++++---------- 2 files changed, 20 insertions(+), 22 deletions(-) (limited to 'ide') diff --git a/ide/coqide.ml b/ide/coqide.ml index 8b164d234c..59b4e3f5eb 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -916,20 +916,12 @@ 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. *) - +(** Create menu items for pairs (query, shortcut key). *) let user_queries_items menu_name item_name l = - 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_for_queries#get^key) else None in + let callback = Query.simplequery (query ^ ".") in + let accel = if not (CString.is_empty key) then + Some (modifier_for_queries#get^key) else None in item (item_name^" "^(no_under query)) ~label:query ?accel ~callback menu_name in List.iter mk_item l diff --git a/ide/preferences.ml b/ide/preferences.ml index f2945a5e07..80e3028fc4 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -929,23 +929,29 @@ 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 input_string l s v = - match GToolbox.input_string ~title:l ~text:s v with - | None -> s + let add_user_query () = + let input_string l v = + match GToolbox.input_string ~title:l v with + | None -> "" | Some s -> s in - let q = input_string "User query" q "Your query" in - let k = input_string "Shortcut key" k "Shortcut (a single letter)" in - q, k + let q = input_string "User query" "Your query" in + let k = input_string "Shortcut key" "Shortcut (a single letter)" in + let last = CString.length q - 1 in + let q = if q.[last] = '.' then CString.sub q 0 last else q in + (* Anything that is not a simple letter will be ignored. *) + let k = + if Int.equal (CString.length k) 1 && Util.is_letter k.[0] then k + else "" in + let k = CString.uppercase 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 () -> ["", ""]) + ~eq:(fun (_, k1) (_, k2) -> k1 = k2) (* Disallow same key. *) + ~add:add_user_query ~titles:["User query"; "Shortcut key"] "User queries" (fun (q, s) -> [q; s]) -- cgit v1.2.3 From 7037e774a0dacbf9335e7fde03ac6932e434343d Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Thu, 2 Jun 2016 12:29:16 +0200 Subject: Dynamic modifier for Queries menu in CoqIDE. --- ide/preferences.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'ide') diff --git a/ide/preferences.ml b/ide/preferences.ml index 80e3028fc4..eec3b72681 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -322,6 +322,7 @@ let _ = attach_modifiers modifier_for_navigation "/Navigation/" let _ = attach_modifiers modifier_for_templates "/Templates/" let _ = attach_modifiers modifier_for_tactics "/Tactics/" let _ = attach_modifiers modifier_for_display "/View/" +let _ = attach_modifiers modifier_for_queries "/Queries/" let modifiers_valid = new preference ~name:["modifiers_valid"] ~init:"" ~repr:Repr.(string) @@ -938,7 +939,8 @@ let configure ?(apply=(fun () -> ())) () = let q = input_string "User query" "Your query" in let k = input_string "Shortcut key" "Shortcut (a single letter)" in let last = CString.length q - 1 in - let q = if q.[last] = '.' then CString.sub q 0 last else q in + let q = if last > 0 && q.[last] = '.' then CString.sub q 0 last else q in + let q = CString.map (fun c -> if c = '$' then ' ' else c) q in (* Anything that is not a simple letter will be ignored. *) let k = if Int.equal (CString.length k) 1 && Util.is_letter k.[0] then k @@ -950,7 +952,8 @@ let configure ?(apply=(fun () -> ())) () = let user_queries = list ~f:user_queries#set - ~eq:(fun (_, k1) (_, k2) -> k1 = k2) (* Disallow same key. *) + (* Disallow same key or empty query. *) + ~eq:(fun (q1, k1) (q2, k2) -> k1 = k2 || q1 = "" || q2 = "") ~add:add_user_query ~titles:["User query"; "Shortcut key"] "User queries" -- cgit v1.2.3 From 5aafa1d18ac4e5c4f61e046faae7b862781ce31d Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Thu, 2 Jun 2016 14:12:22 +0200 Subject: User queries can be terminated with "...". This appends the currently selected word to the query. Only queries that end with this are supported, "..." inside the query will just not work. --- ide/coqide.ml | 24 +++++++++++++----------- ide/coqide_ui.ml | 2 +- ide/preferences.ml | 6 ++---- 3 files changed, 16 insertions(+), 16 deletions(-) (limited to 'ide') diff --git a/ide/coqide.ml b/ide/coqide.ml index 59b4e3f5eb..d1a799a773 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -682,10 +682,13 @@ let doquery query sn = Coq.try_grab sn.coqtop (sn.coqops#raw_coq_query query) ignore let otherquery command sn = - let word = get_current_word sn in - if word <> "" then - let query = command ^ " " ^ word ^ "." in - doquery query sn + Option.iter (fun query -> doquery (query ^ ".") sn) + begin try + let i = CString.string_index_from command 0 "..." in + let word = get_current_word sn in + if word = "" then None + else Some (CString.sub command 0 i ^ " " ^ word) + with Not_found -> Some command end let otherquery command = cb_on_current_term (otherquery command) @@ -694,8 +697,6 @@ let query command _ = then searchabout () else otherquery command () -let simplequery query = cb_on_current_term (doquery query) - end (** Misc *) @@ -919,7 +920,7 @@ let template_item (text, offset, len, key) = (** Create menu items for pairs (query, shortcut key). *) let user_queries_items menu_name item_name l = let mk_item (query, key) = - let callback = Query.simplequery (query ^ ".") in + let callback = Query.query query in let accel = if not (CString.is_empty key) then Some (modifier_for_queries#get^key) else None in item (item_name^" "^(no_under query)) ~label:query ?accel ~callback menu_name @@ -1115,21 +1116,22 @@ let build_ui () = ]; alpha_items templates_menu "Template" Coq_commands.commands; - let qitem s sc = + let qitem s sc ?(dots = true) = + let query = if dots then s ^ "..." else s in item s ~label:("_"^s) ~accel:(modifier_for_queries#get^sc) - ~callback:(Query.query s) + ~callback:(Query.query query) in menu queries_menu [ item "Queries" ~label:"_Queries"; - qitem "Search" "K"; + qitem "Search" "K" ~dots:false; qitem "Check" "C"; qitem "Print" "P"; qitem "About" "A"; qitem "Locate" "L"; qitem "Print Assumptions" "N"; ]; - user_queries_items queries_menu "Query" user_queries#get; + user_queries_items queries_menu "User-Query" user_queries#get; menu tools_menu [ item "Tools" ~label:"_Tools"; diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index b45a9f12b8..2ae18593ac 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -173,6 +173,6 @@ let init () = (if Coq_config.gtk_platform <> `QUARTZ then "" 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)) + (Buffer.contents (list_queries "User-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 eec3b72681..3a33bbb1d8 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -938,8 +938,6 @@ let configure ?(apply=(fun () -> ())) () = in let q = input_string "User query" "Your query" in let k = input_string "Shortcut key" "Shortcut (a single letter)" in - let last = CString.length q - 1 in - let q = if last > 0 && q.[last] = '.' then CString.sub q 0 last else q in let q = CString.map (fun c -> if c = '$' then ' ' else c) q in (* Anything that is not a simple letter will be ignored. *) let k = @@ -952,8 +950,8 @@ let configure ?(apply=(fun () -> ())) () = let user_queries = list ~f:user_queries#set - (* Disallow same key or empty query. *) - ~eq:(fun (q1, k1) (q2, k2) -> k1 = k2 || q1 = "" || q2 = "") + (* Disallow same query, key or empty query. *) + ~eq:(fun (q1, k1) (q2, k2) -> k1 = k2 || q1 = "" || q2 = "" || q1 = q2) ~add:add_user_query ~titles:["User query"; "Shortcut key"] "User queries" -- cgit v1.2.3