diff options
| -rw-r--r-- | ide/coqide.ml | 24 | ||||
| -rw-r--r-- | ide/coqide_ui.ml | 2 | ||||
| -rw-r--r-- | ide/preferences.ml | 6 |
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" |