diff options
| author |  Cyprien Mangin <cyprien.mangin@m4x.org> | 2015-07-07 14:04:09 +0200 |
|---|---|---|
| committer | Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-02 11:30:02 +0200 |
| commit | 2911de377786ad525dd9407968dae7c1973d7190 (patch) | |
| tree | 5502e8000752c23af3bc62443b9d433c49fbae40 /ide/preferences.ml | |
| parent | 5874843ea8e1ca82f8b1b646022582309b7fe24c (diff) | |
Slightly better interface to edit queries.
Diffstat (limited to 'ide/preferences.ml')
| -rw-r--r-- | ide/preferences.ml | 9 |
1 files changed, 7 insertions, 2 deletions
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 |