[coqtop] handle -print-module-uid after initialization

4 files changed, 22 insertions, 17 deletions

diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml
index 2941497c12..b42c705add 100644
--- a/ide/coqide/idetop.ml
+++ b/ide/coqide/idetop.ml
@@ -516,7 +516,8 @@ let msg_format = ref (fun () ->
 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 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;
diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index bb0c4882e6..19350b7e98 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -220,15 +220,6 @@ let get_float ~opt n =
   with Failure _ ->
     error_wrong_arg ("Error: float expected after option "^opt)
 
-let get_native_name s =
-  (* We ignore even critical errors because this mode has to be super silent *)
-  try
-    Filename.(List.fold_left concat (dirname s)
-                [ !Nativelib.output_dir
-                ; Library.native_name_from_filename s
-                ])
-  with _ -> ""
-
 let interp_set_option opt v old =
   let open Goptions in
   let opt = String.concat " " opt in
@@ -361,9 +352,6 @@ let parse_args ~usage ~init arglist : t * string list =
       Goptions.set_string_option_value ["Mangle"; "Names"; "Prefix"] (next ());
       oval
 
-    |"-print-mod-uid" ->
-      let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0
-
     |"-profile-ltac-cutoff" ->
       Flags.profile_ltac := true;
       Flags.profile_ltac_cutoff := get_float ~opt (next ());
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 714af6f51a..caf86ef870 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -143,7 +143,8 @@ let print_style_tags opts =
   let () = List.iter iter tags in
   flush_all ()
 
-type run_mode = Interactive | Batch | Query_PrintTags
+type query = PrintTags | PrintModUid of string list
+type run_mode = Interactive | Batch | Query of query
 
 type toplevel_options = {
   run_mode : run_mode;
@@ -197,7 +198,8 @@ let parse_extra_colors extras =
 let coqtop_parse_extra extras =
   let rec parse_extra run_mode  = function
   | "-batch" :: rest -> parse_extra Batch  rest
-  | x :: rest ->
+  | "-print-mod-uid" :: rest -> Query (PrintModUid rest), []
+  |   x :: rest ->
     let run_mode, rest = parse_extra run_mode rest in run_mode, x :: rest
   | [] -> run_mode, [] in
   let run_mode, extras = parse_extra Interactive extras in
@@ -205,10 +207,23 @@ let coqtop_parse_extra extras =
   let async_opts, extras = Stmargs.parse_args ~init:Stm.AsyncOpts.default_opts extras in
   ({ run_mode; color_mode}, async_opts), extras
 
+let get_native_name s =
+  (* We ignore even critical errors because this mode has to be super silent *)
+  try
+    Filename.(List.fold_left concat (dirname s)
+                [ !Nativelib.output_dir
+                ; Library.native_name_from_filename s
+                ])
+  with _ -> ""
+
 let coqtop_run ({ run_mode; color_mode },_) ~opts state =
   match run_mode with
   | Interactive -> Coqloop.loop ~opts ~state;
-  | Query_PrintTags -> print_style_tags color_mode; exit 0
+  | Query PrintTags -> print_style_tags color_mode; exit 0
+  | Query (PrintModUid sl) ->
+      let s = String.concat " " (List.map get_native_name sl) in
+      print_endline s;
+      exit 0
   | Batch -> exit 0
 
 let coqtop_specific_usage = Usage.{
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index f51df102bd..c675c6adec 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -42,7 +42,8 @@ val init_toploop : Coqargs.t -> Stm.AsyncOpts.stm_opt -> Coqargs.injection_comma
 
 (** The specific characterization of the coqtop_toplevel *)
 
-type run_mode = Interactive | Batch | Query_PrintTags
+type query = PrintTags | PrintModUid of string list
+type run_mode = Interactive | Batch | Query of query
 
 type toplevel_options = {
   run_mode : run_mode;