diff options
| -rw-r--r-- | ide/coqide.ml | 16 | ||||
| -rw-r--r-- | ide/preferences.ml | 26 |
2 files changed, 20 insertions, 22 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 8b164d234..59b4e3f5e 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 f2945a5e0..80e3028fc 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 () -> ["<user query>", "<shortcut key>"]) + ~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]) |