diff options
| author |  Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-02 14:12:22 +0200 |
|---|---|---|
| committer | Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-02 14:12:22 +0200 |
| commit | 5aafa1d18ac4e5c4f61e046faae7b862781ce31d (patch) | |
| tree | 1e014c1d5ae6e4d62cb43b2a1f1c52d854ec6634 /ide/preferences.ml | |
| parent | 7037e774a0dacbf9335e7fde03ac6932e434343d (diff) | |
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.
Diffstat (limited to 'ide/preferences.ml')
| -rw-r--r-- | ide/preferences.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index eec3b7268..3a33bbb1d 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" |