aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/coqide/coq.ml21
-rw-r--r--ide/coqide/coq_commands.ml1
-rw-r--r--ide/coqide/coqide.ml6
-rw-r--r--ide/coqide/coqide_main.ml2
-rw-r--r--ide/coqide/dune4
-rw-r--r--ide/coqide/idetop.ml36
-rw-r--r--ide/coqide/microPG.ml2
-rw-r--r--ide/coqide/protocol/dune2
-rw-r--r--ide/coqide/wg_Find.ml16
-rw-r--r--ide/coqide/wg_ProofView.ml8
10 files changed, 47 insertions, 51 deletions
diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml
index b8228df2aa..20e9f0134f 100644
--- a/ide/coqide/coq.ml
+++ b/ide/coqide/coq.ml
@@ -13,13 +13,9 @@ open Preferences
let ideslave_coqtop_flags = ref None
-(** * Version and date *)
+(** * Version *)
-let get_version_date () =
- let date =
- if Glib.Utf8.validate Coq_config.date
- then Coq_config.date
- else "<date not printable>" in
+let get_version () =
try
(* the following makes sense only when running with local layout *)
let coqroot = Filename.concat
@@ -29,21 +25,20 @@ let get_version_date () =
let ch = open_in (Filename.concat coqroot "revision") in
let ver = input_line ch in
let rev = input_line ch in
- (ver,rev)
- with _ -> (Coq_config.version,date)
+ close_in ch;
+ Printf.sprintf "%s (%s)" ver rev
+ with _ -> Coq_config.version
let short_version () =
- let (ver,date) = get_version_date () in
- Printf.sprintf "The Coq Proof Assistant, version %s (%s)\n" ver date
+ Printf.sprintf "The Coq Proof Assistant, version %s\n" (get_version ())
let version () =
- let (ver,date) = get_version_date () in
Printf.sprintf
- "The Coq Proof Assistant, version %s (%s)\
+ "The Coq Proof Assistant, version %s\
\nArchitecture %s running %s operating system\
\nGtk version is %s\
\nThis is %s \n"
- ver date
+ (get_version ())
Coq_config.arch Sys.os_type
(let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z)
(Filename.basename Sys.executable_name)
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..3fbfbd66d3 100644
--- a/ide/coqide/coqide.ml
+++ b/ide/coqide/coqide.ml
@@ -1374,8 +1374,7 @@ let main files =
let read_coqide_args argv =
let set_debug () =
Minilib.debug := true;
- Flags.debug := true;
- Exninfo.record_backtrace true
+ CDebug.set_debug_all true
in
let rec filter_coqtop coqtop project_files bindings_files out = function
|"-unicode-bindings" :: sfilenames :: args ->
@@ -1405,6 +1404,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/coqide_main.ml b/ide/coqide/coqide_main.ml
index 0812e00960..a178e72806 100644
--- a/ide/coqide/coqide_main.ml
+++ b/ide/coqide/coqide_main.ml
@@ -35,7 +35,7 @@ let catch_gtk_messages () =
let () = GToolbox.message_box ~title:"Error" (header ^ msg) in
Coqide.crash_save 1
|`ERROR ->
- if !Flags.debug then GToolbox.message_box ~title:"Error" (header ^ msg)
+ if CDebug.(get_flag misc) then GToolbox.message_box ~title:"Error" (header ^ msg)
else Printf.eprintf "%s\n" (header ^ msg)
|`DEBUG -> Minilib.log msg
|level when Sys.os_type = "Win32" -> Minilib.log ~level msg
diff --git a/ide/coqide/dune b/ide/coqide/dune
index 12bad7ebc4..4bb4672cd4 100644
--- a/ide/coqide/dune
+++ b/ide/coqide/dune
@@ -6,7 +6,7 @@
(public_name coqide-server.core)
(wrapped false)
(modules document)
- (libraries coq.lib))
+ (libraries coq-core.lib))
(executable
(name fake_ide)
@@ -20,7 +20,7 @@
(public_name coqidetop.opt)
(package coqide-server)
(modules idetop)
- (libraries coq.toplevel coqide-server.protocol)
+ (libraries coq-core.toplevel coqide-server.protocol)
(modes native byte)
(link_flags -linkall))
diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml
index 528e2a756b..a6a7f7d742 100644
--- a/ide/coqide/idetop.ml
+++ b/ide/coqide/idetop.ml
@@ -35,11 +35,11 @@ let pr_with_pid s = Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s
let pr_error s = pr_with_pid s
let pr_debug s =
- if !Flags.debug then pr_with_pid s
+ if CDebug.(get_flag misc) then pr_with_pid s
let pr_debug_call q =
- if !Flags.debug then pr_with_pid ("<-- " ^ Xmlprotocol.pr_call q)
+ if CDebug.(get_flag misc) then pr_with_pid ("<-- " ^ Xmlprotocol.pr_call q)
let pr_debug_answer q r =
- if !Flags.debug then pr_with_pid ("--> " ^ Xmlprotocol.pr_full_value q r)
+ if CDebug.(get_flag misc) then pr_with_pid ("--> " ^ Xmlprotocol.pr_full_value q r)
(** Categories of commands *)
@@ -397,8 +397,8 @@ let set_options options =
let about () = {
Interface.coqtop_version = Coq_config.version;
Interface.protocol_version = Xmlprotocol.protocol_version;
- Interface.release_date = Coq_config.date;
- Interface.compile_date = Coq_config.compile_date;
+ Interface.release_date = "n/a";
+ Interface.compile_date = "n/a";
}
let handle_exn (e, info) =
@@ -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/microPG.ml b/ide/coqide/microPG.ml
index 5a4871b70a..9908703cea 100644
--- a/ide/coqide/microPG.ml
+++ b/ide/coqide/microPG.ml
@@ -15,7 +15,7 @@ open GdkKeysyms
open Printf
let eprintf x =
- if !Flags.debug then Printf.eprintf x else Printf.ifprintf stderr x
+ if CDebug.(get_flag misc) then Printf.eprintf x else Printf.ifprintf stderr x
type gui = {
notebook : session Wg_Notebook.typed_notebook;
diff --git a/ide/coqide/protocol/dune b/ide/coqide/protocol/dune
index 801ceb20ec..f48c7de0c4 100644
--- a/ide/coqide/protocol/dune
+++ b/ide/coqide/protocol/dune
@@ -2,6 +2,6 @@
(name protocol)
(public_name coqide-server.protocol)
(wrapped false)
- (libraries coq.lib))
+ (libraries coq-core.lib))
(ocamllex xml_lexer)
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"
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 00:16:56 +0000