diff options
| author | Enrico Tassi | 2021-01-06 17:13:59 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2021-01-27 09:45:49 +0100 |
| commit | f5ec3f5cbd4bc2e0f65e1c52143b199ce7c2a5ad (patch) | |
| tree | 5b8287e69fcc7e782d2095cc0008cf5fedf47ae3 /toplevel | |
| parent | b9bac1d7ef4a4c06ebe842ffd9aac322186a65d3 (diff) | |
[coqtop] handle -print-module-uid after initialization
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 21 | ||||
| -rw-r--r-- | toplevel/coqtop.mli | 3 |
2 files changed, 20 insertions, 4 deletions
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; |