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.

3 files changed, 16 insertions, 16 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 59b4e3f5e..d1a799a77 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -682,10 +682,13 @@ let doquery query sn =
   Coq.try_grab sn.coqtop (sn.coqops#raw_coq_query query) ignore
 
 let otherquery command sn =
-  let word = get_current_word sn in
-  if word <> "" then
-    let query = command ^ " " ^ word ^ "." in
-    doquery query sn
+  Option.iter (fun query -> doquery (query ^ ".") sn)
+    begin try
+      let i = CString.string_index_from command 0 "..." in
+      let word = get_current_word sn in
+      if word = "" then None
+      else Some (CString.sub command 0 i ^ " " ^ word)
+    with Not_found -> Some command end
 
 let otherquery command = cb_on_current_term (otherquery command)
 
@@ -694,8 +697,6 @@ let query command _ =
   then searchabout ()
   else otherquery command ()
 
-let simplequery query = cb_on_current_term (doquery query)
-
 end
 
 (** Misc *)
@@ -919,7 +920,7 @@ let template_item (text, offset, len, key) =
 (** Create menu items for pairs (query, shortcut key). *)
 let user_queries_items menu_name item_name l =
   let mk_item (query, key) =
-    let callback = Query.simplequery (query ^ ".") in
+    let callback = Query.query 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
@@ -1115,21 +1116,22 @@ let build_ui () =
   ];
   alpha_items templates_menu "Template" Coq_commands.commands;
 
-  let qitem s sc =
+  let qitem s sc ?(dots = true) =
+    let query = if dots then s ^ "..." else s in
     item s ~label:("_"^s)
       ~accel:(modifier_for_queries#get^sc)
-      ~callback:(Query.query s)
+      ~callback:(Query.query query)
   in
   menu queries_menu [
     item "Queries" ~label:"_Queries";
-    qitem "Search" "K";
+    qitem "Search" "K" ~dots:false;
     qitem "Check" "C";
     qitem "Print" "P";
     qitem "About" "A";
     qitem "Locate" "L";
     qitem "Print Assumptions" "N";
   ];
-  user_queries_items queries_menu "Query" user_queries#get;
+  user_queries_items queries_menu "User-Query" user_queries#get;
 
   menu tools_menu [
     item "Tools" ~label:"_Tools";
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index b45a9f12b..2ae18593a 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -173,6 +173,6 @@ let init () =
     (if Coq_config.gtk_platform <> `QUARTZ then "<menuitem action='Quit' />" else "")
     (Buffer.contents (list_items "Tactic" Coq_commands.tactics))
     (Buffer.contents (list_items "Template" Coq_commands.commands))
-    (Buffer.contents (list_queries "Query" Preferences.user_queries#get))
+    (Buffer.contents (list_queries "User-Query" Preferences.user_queries#get))
  in
   ignore (ui_m#add_ui_from_string theui);
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"