Add user-created queries to CoqIDE.

4 files changed, 73 insertions, 10 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 2d1ba72f3..8697ca833 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -681,10 +681,6 @@ let doquery query sn =
   sn.messages#clear;
   Coq.try_grab sn.coqtop (sn.coqops#raw_coq_query query) ignore
 
-let showproof () =
-  let query = "Show Proof." in
-  on_current_term (doquery query)
-
 let otherquery command sn =
   let word = get_current_word sn in
   if word <> "" then
@@ -696,10 +692,10 @@ let otherquery command = cb_on_current_term (otherquery command)
 let query command _ =
   if command = "Search" || command = "SearchAbout"
   then searchabout ()
-  else if command = "Show Proof"
-  then showproof ()
   else otherquery command ()
 
+let simplequery query = cb_on_current_term (doquery query)
+
 end
 
 (** Misc *)
@@ -868,12 +864,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
@@ -920,6 +916,24 @@ 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).
+    If the shortcut key is not in the range 'a'-'z','A'-'Z', it will be ignored.  *)
+
+let user_queries_items menu_name item_name l modifier =
+  let valid_key k = Int.equal (CString.length k) 1 && Util.is_letter k.[0] in
+  let mk_item (query, key) =
+    let query' =
+      let last = CString.length query - 1 in
+      if query.[last] = '.'
+      then query
+      else query ^ "."
+    in
+    let callback = Query.simplequery query' in
+    let accel = if valid_key key then Some (modifier^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
@@ -1120,6 +1134,7 @@ let build_ui () =
     qitem "Print Assumptions" (Some "<Ctrl><Shift>N");
     qitem "Show Proof" (Some "<Ctrl><Shift>R");
   ];
+  user_queries_items queries_menu "Query" user_queries#get "<Ctrl><Shift>";
 
   menu tools_menu [
     item "Tools" ~label:"_Tools";
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index 65735240a..b45a9f12b 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,7 +128,8 @@ let init () =
     <menuitem action='About' />
     <menuitem action='Locate' />
     <menuitem action='Print Assumptions' />
-    <menuitem action='Show Proof' />
+    <separator />
+    %s
   </menu>
   <menu name='Tools' action='Tools'>
     <menuitem action='Comment' />
@@ -163,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 "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..b7fdc975c 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]
@@ -507,6 +519,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)
 
@@ -908,6 +923,25 @@ let configure ?(apply=(fun () -> ())) () =
   let misc = [contextual_menus_on_goal;stop_before;reset_on_tab_switch;
               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
+      q, k
+  in
+
+  let user_queries =
+    list
+      ~f:user_queries#set
+      ~eq:(fun (q1, _) (q2, _) -> q1 = q2)
+      ~edit:edit_user_query
+      ~add:(fun () -> ["<user query>", "<shortcut key>"])
+      ~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 =
@@ -939,7 +973,9 @@ let configure ?(apply=(fun () -> ())) () =
 	     [modifiers_valid; modifier_for_tactics;
 	      modifier_for_templates; modifier_for_display; modifier_for_navigation]);
      Section("Misc", Some `ADD,
-	     misc)]
+       misc);
+     Section("User queries", None,
+       [user_queries])]
   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..ebcff2080 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -95,6 +95,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