diff options
| -rw-r--r-- | ide/coqide/idetop.ml | 3 | ||||
| -rw-r--r-- | sysinit/coqargs.ml | 12 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 21 | ||||
| -rw-r--r-- | toplevel/coqtop.mli | 3 |
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; |