Merge PR #190: Add configurable shortcuts for user queries to CoqIDE.

4 files changed, 105 insertions, 16 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 758a5a4c9..d1a799a77 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -677,12 +677,18 @@ let searchabout sn =
 
 let searchabout () = on_current_term searchabout
 
+let doquery query sn =
+  sn.messages#clear;
+  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
-    sn.messages#clear;
-    Coq.try_grab sn.coqtop (sn.coqops#raw_coq_query query) ignore
+  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)
 
@@ -859,12 +865,12 @@ let toggle_items menu_name l =
   in
   List.iter f l
 
+let no_under = Util.String.map (fun x -> if x = '_' then '-' else x)
+
 (** Create alphabetical menu items with elements in sub-items.
     [l] is a list of lists, one per initial letter *)
 
 let alpha_items menu_name item_name l =
-  let no_under = Util.String.map (fun x -> if x = '_' then '-' else x)
-  in
   let mk_item text =
     let text' =
       let last = String.length text - 1 in
@@ -911,6 +917,16 @@ let template_item (text, offset, len, key) =
   in
   item name ~label ~callback:(cb_on_current_term callback) ~accel:(modifier^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.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
+  in
+  List.iter mk_item l
+
 let emit_to_focus window sgn =
   let focussed_widget = GtkWindow.Window.get_focus window#as_window in
   let obj = Gobject.unsafe_cast focussed_widget in
@@ -1100,16 +1116,22 @@ let build_ui () =
   ];
   alpha_items templates_menu "Template" Coq_commands.commands;
 
-  let qitem s accel = item s ~label:("_"^s) ?accel ~callback:(Query.query s) in
+  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 query)
+  in
   menu queries_menu [
     item "Queries" ~label:"_Queries";
-    qitem "Search" (Some "<Ctrl><Shift>K");
-    qitem "Check" (Some "<Ctrl><Shift>C");
-    qitem "Print" (Some "<Ctrl><Shift>P");
-    qitem "About" (Some "<Ctrl><Shift>A");
-    qitem "Locate" (Some "<Ctrl><Shift>L");
-    qitem "Print Assumptions" (Some "<Ctrl><Shift>N");
+    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 "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 edfe28b26..2ae18593a 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -18,6 +18,15 @@ let list_items menu li =
   let () = List.iter (fun b -> Buffer.add_buffer res_buf (tactic_item b)) li in
   res_buf
 
+let list_queries menu li =
+  let res_buf = Buffer.create 500 in
+  let query_item (q, _) =
+    let s = "<menuitem action='"^menu^" "^(no_under q)^"' />\n" in
+    Buffer.add_string res_buf s
+  in
+  let () = List.iter query_item li in
+  res_buf
+
 let init () =
   let theui = Printf.sprintf "<ui>
 <menubar name='CoqIde MenuBar'>
@@ -119,6 +128,8 @@ let init () =
     <menuitem action='About' />
     <menuitem action='Locate' />
     <menuitem action='Print Assumptions' />
+    <separator />
+    %s
   </menu>
   <menu name='Tools' action='Tools'>
     <menuitem action='Comment' />
@@ -162,5 +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 "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 c4dc55972..3a33bbb1d 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -144,6 +144,18 @@ object
   method into s = Some s
 end
 
+let string_pair_list (sep : char) : (string * string) list repr =
+object
+  val sep' = String.make 1 sep
+  method from = CList.map (fun (s1, s2) -> CString.concat sep' [s1; s2])
+  method into l =
+    try
+      Some (CList.map (fun s ->
+        let split = CString.split sep s in
+        CList.nth split 0, CList.nth split 1) l)
+    with Failure _ -> None
+end
+
 let bool : bool repr =
 object
   method from s = [string_of_bool s]
@@ -303,10 +315,14 @@ let modifier_for_tactics =
 let modifier_for_display =
   new preference ~name:["modifier_for_display"] ~init:"<Alt><Shift>" ~repr:Repr.(string)
 
+let modifier_for_queries =
+  new preference ~name:["modifier_for_queries"] ~init:"<Control><Shift>" ~repr:Repr.(string)
+
 let _ = attach_modifiers modifier_for_navigation "<Actions>/Navigation/"
 let _ = attach_modifiers modifier_for_templates "<Actions>/Templates/"
 let _ = attach_modifiers modifier_for_tactics "<Actions>/Tactics/"
 let _ = attach_modifiers modifier_for_display "<Actions>/View/"
+let _ = attach_modifiers modifier_for_queries "<Actions>/Queries/"
 
 let modifiers_valid =
   new preference ~name:["modifiers_valid"] ~init:"<Alt><Control><Shift>" ~repr:Repr.(string)
@@ -507,6 +523,9 @@ let highlight_current_line =
 let nanoPG =
   new preference ~name:["nanoPG"] ~init:false ~repr:Repr.(bool)
 
+let user_queries =
+  new preference ~name:["user_queries"] ~init:[] ~repr:Repr.(string_pair_list '$')
+
 class tag_button (box : Gtk.box Gtk.obj) =
 object (self)
 
@@ -837,6 +856,9 @@ let configure ?(apply=(fun () -> ())) () =
   let modifier_for_display =
     pmodifiers "Modifiers for View Menu" modifier_for_display
   in
+  let modifier_for_queries =
+    pmodifiers "Modifiers for Queries Menu" modifier_for_queries
+  in
   let modifiers_valid =
     pmodifiers ~all:true "Allowed modifiers" modifiers_valid
   in
@@ -908,6 +930,36 @@ let configure ?(apply=(fun () -> ())) () =
   let misc = [contextual_menus_on_goal;stop_before;reset_on_tab_switch;
               vertical_tabs;opposite_tabs] in
 
+  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" "Your query" in
+    let k = input_string "Shortcut key" "Shortcut (a single letter)" 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 =
+      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
+      (* 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"
+      (fun (q, s) -> [q; s])
+      user_queries#get
+
+  in
+
 (* ATTENTION !!!!! L'onglet Fonts doit etre en premier pour eviter un bug !!!!
    (shame on Benjamin) *)
   let cmds =
@@ -937,9 +989,10 @@ let configure ?(apply=(fun () -> ())) () =
 	     [automatic_tactics]);
      Section("Shortcuts", Some `PREFERENCES,
 	     [modifiers_valid; modifier_for_tactics;
-	      modifier_for_templates; modifier_for_display; modifier_for_navigation]);
+        modifier_for_templates; modifier_for_display; modifier_for_navigation;
+        modifier_for_queries; user_queries]);
      Section("Misc", Some `ADD,
-	     misc)]
+       misc)]
   in
 (*
   Format.printf "before edit: current.text_font = %s@." (Pango.Font.to_string current.text_font);
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 1733091a5..426b0a328 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -65,6 +65,7 @@ val modifier_for_navigation : string preference
 val modifier_for_templates : string preference
 val modifier_for_tactics : string preference
 val modifier_for_display : string preference
+val modifier_for_queries : string preference
 val modifiers_valid : string preference
 val cmd_browse : string preference
 val cmd_editor : string preference
@@ -95,6 +96,7 @@ val spaces_instead_of_tabs : bool preference
 val tab_length : int preference
 val highlight_current_line : bool preference
 val nanoPG : bool preference
+val user_queries : (string * string) list preference
 
 val save_pref : unit -> unit
 val load_pref : unit -> unit