diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide/coq_commands.ml | 1 | ||||
| -rw-r--r-- | ide/coqide/coqide.ml | 3 | ||||
| -rw-r--r-- | ide/coqide/idetop.ml | 26 | ||||
| -rw-r--r-- | ide/coqide/wg_Find.ml | 16 | ||||
| -rw-r--r-- | ide/coqide/wg_ProofView.ml | 8 |
5 files changed, 28 insertions, 26 deletions
diff --git a/ide/coqide/coq_commands.ml b/ide/coqide/coq_commands.ml index 711986c2b2..2d75ad9ff6 100644 --- a/ide/coqide/coq_commands.ml +++ b/ide/coqide/coq_commands.ml @@ -207,7 +207,6 @@ let state_preserving = [ "Recursive Extraction Library"; "Search"; - "SearchHead"; "SearchPattern"; "SearchRewrite"; diff --git a/ide/coqide/coqide.ml b/ide/coqide/coqide.ml index f9e6e74372..e066fc6292 100644 --- a/ide/coqide/coqide.ml +++ b/ide/coqide/coqide.ml @@ -1405,6 +1405,9 @@ let read_coqide_args argv = |"-coqtop-flags" :: flags :: args-> Coq.ideslave_coqtop_flags := Some flags; filter_coqtop coqtop project_files bindings_files out args + | ("-v" | "--version") :: _ -> + Printf.printf "CoqIDE, version %s\n" Coq_config.version; + exit 0 |arg::args when out = [] && CString.is_prefix "-psn_" arg -> (* argument added by MacOS during .app launch *) filter_coqtop coqtop project_files bindings_files out args diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index 528e2a756b..b42c705add 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -513,9 +513,11 @@ let msg_format = ref (fun () -> (* The loop ignores the command line arguments as the current model delegates its handing to the toplevel container. *) -let loop run_mode ~opts:_ state = +let loop ( { Coqtop.run_mode; color_mode },_) ~opts:_ state = match run_mode with | Coqtop.Batch -> exit 0 + | Coqtop.(Query PrintTags) -> Coqtop.print_style_tags color_mode; exit 0 + | Coqtop.(Query _) -> Printf.eprintf "Unknown query"; exit 1 | Coqtop.Interactive -> let open Vernac.State in set_doc state.doc; @@ -580,32 +582,28 @@ coqidetop specific options:\n\ \n --help-XML-protocol print documentation of the Coq XML protocol\n" } -let islave_parse ~opts extra_args = +let islave_parse extra_args = let open Coqtop in - let run_mode, extra_args = coqtop_toplevel.parse_extra ~opts extra_args in + let ({ run_mode; color_mode }, stm_opts), extra_args = coqtop_toplevel.parse_extra extra_args in let extra_args = parse extra_args in (* One of the role of coqidetop is to find the name of buffers to open *) (* in the command line; Coqide is waiting these names on stdout *) (* (see filter_coq_opts in coq.ml), so we send them now *) print_string (String.concat "\n" extra_args); - run_mode, [] + ( { Coqtop.run_mode; color_mode }, stm_opts), [] -let islave_init run_mode ~opts = +let islave_init ( { Coqtop.run_mode; color_mode }, stm_opts) injections ~opts = if run_mode = Coqtop.Batch then Flags.quiet := true; - Coqtop.init_toploop opts + Coqtop.init_toploop opts stm_opts injections -let islave_default_opts = - Coqargs.{ default with - config = { default.config with - stm_flags = { default.config.stm_flags with - Stm.AsyncOpts.async_proofs_worker_priority = CoqworkmgrApi.High }}} +let islave_default_opts = Coqargs.default let () = let open Coqtop in let custom = { parse_extra = islave_parse ; - help = coqidetop_specific_usage; - init = islave_init; + usage = coqidetop_specific_usage; + init_extra = islave_init; run = loop; - opts = islave_default_opts } in + initial_args = islave_default_opts } in start_coq custom diff --git a/ide/coqide/wg_Find.ml b/ide/coqide/wg_Find.ml index 7e89191bd1..7f30cc8c6c 100644 --- a/ide/coqide/wg_Find.ml +++ b/ide/coqide/wg_Find.ml @@ -219,16 +219,18 @@ class finder name (view : GText.view) = let _ = replace_all_button#connect#clicked ~callback:self#replace_all in (* Keypress interaction *) - let generic_cb esc_cb ret_cb ev = + let dispatch_key_cb esc_cb ret_cb shift_ret_cb ev = let ev_key = GdkEvent.Key.keyval ev in - let (return, _) = GtkData.AccelGroup.parse "Return" in - let (esc, _) = GtkData.AccelGroup.parse "Escape" in - if ev_key = return then (ret_cb (); true) - else if ev_key = esc then (esc_cb (); true) + let ev_modifiers = GdkEvent.Key.state ev in + if ev_key = GdkKeysyms._Return then + (if List.mem `SHIFT ev_modifiers then + shift_ret_cb () + else ret_cb (); true) + else if ev_key = GdkKeysyms._Escape then (esc_cb (); true) else false in - let find_cb = generic_cb self#hide self#find_forward in - let replace_cb = generic_cb self#hide self#replace in + let find_cb = dispatch_key_cb self#hide self#find_forward self#find_backward in + let replace_cb = dispatch_key_cb self#hide self#replace self#replace in let _ = find_entry#event#connect#key_press ~callback:find_cb in let _ = replace_entry#event#connect#key_press ~callback:replace_cb in diff --git a/ide/coqide/wg_ProofView.ml b/ide/coqide/wg_ProofView.ml index 01dfed0067..fa37edd82b 100644 --- a/ide/coqide/wg_ProofView.ml +++ b/ide/coqide/wg_ProofView.ml @@ -66,7 +66,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = mat in let goals_cnt = List.length rem_goals + 1 in let head_str = Printf.sprintf - "%d subgoal%s\n" goals_cnt (if 1 < goals_cnt then "s" else "") + "%d goal%s\n" goals_cnt (if 1 < goals_cnt then "s" else "") in let goal_str ?(shownum=false) index total id = let annot = @@ -148,10 +148,10 @@ let display mode (view : #GText.view_skel) goals hints evars = let evars = match evars with None -> [] | Some evs -> evs in begin match (bg, shelved_goals,given_up_goals, evars) with | [], [], [], [] -> - view#buffer#insert "No more subgoals." + view#buffer#insert "No more goals." | [], [], [], _ :: _ -> (* A proof has been finished, but not concluded *) - view#buffer#insert "No more subgoals, but there are non-instantiated existential variables:\n\n"; + view#buffer#insert "No more goals, but there are non-instantiated existential variables:\n\n"; let iter evar = let msg = Printf.sprintf "%s\n" evar.Interface.evar_info in view#buffer#insert msg @@ -160,7 +160,7 @@ let display mode (view : #GText.view_skel) goals hints evars = view#buffer#insert "\nYou can use Grab Existential Variables." | [], [], _, _ -> (* The proof is finished, with the exception of given up goals. *) - view#buffer#insert "No more subgoals, but there are some goals you gave up:\n\n"; + view#buffer#insert "No more goals, but there are some goals you gave up:\n\n"; let iter goal = insert_xml view#buffer (Richpp.richpp_of_pp width goal.Interface.goal_ccl); view#buffer#insert "\n" |