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/preferences.ml | 26 ++++++++++++++++---------- 1 file changed, 16 insertions(+), 10 deletions(-) (limited to 'ide/preferences.ml') 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 () -> ["", ""]) + ~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