From 2911de377786ad525dd9407968dae7c1973d7190 Mon Sep 17 00:00:00 2001
From: Cyprien Mangin <cyprien.mangin@m4x.org>
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/preferences.ml')

diff --git a/ide/preferences.ml b/ide/preferences.ml
index b7fdc975c..b39a1106c 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