diff options
| -rw-r--r-- | ide/coq.ml | 2 | ||||
| -rw-r--r-- | ide/idetop.ml | 23 | ||||
| -rw-r--r-- | toplevel/coqc.ml | 16 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 24 | ||||
| -rw-r--r-- | toplevel/coqtop.mli | 18 | ||||
| -rw-r--r-- | toplevel/workerLoop.ml | 13 |
6 files changed, 62 insertions, 34 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 92c24b3b85..889cc3be36 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -102,7 +102,7 @@ let display_coqtop_answer cmd lines = let rec filter_coq_opts args = let argstr = String.concat " " (List.map Filename.quote args) in - let cmd = Filename.quote (coqtop_path ()) ^" -nois -filteropts " ^ argstr in + let cmd = Filename.quote (coqtop_path ()) ^" -nois -batch " ^ argstr in let cmd = requote cmd in let filtered_args = ref [] in let errlines = ref [] in diff --git a/ide/idetop.ml b/ide/idetop.ml index c6a8fdaa55..c7638343b0 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -553,12 +553,25 @@ let () = Usage.add_to_usage "coqidetop" " --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\ \n --help-XML-protocol print documentation of the Coq XML protocol\n" -let islave_init ~opts extra_args = - let args = parse extra_args in - CoqworkmgrApi.(init High); - opts, args +let islave_parse ~opts extra_args = + let open Coqtop in + let run_mode, extra_args = coqtop_toplevel.parse_extra ~opts 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, [] + +let islave_init ~opts = + CoqworkmgrApi.(init High) let () = let open Coqtop in - let custom = { init = islave_init; run = loop; opts = Coqargs.default } in + let custom = { + parse_extra = islave_parse ; + help = (fun _ -> output_string stderr "Same options as coqtop"); + init = islave_init; + run = loop; + opts = Coqargs.default } in start_coq custom diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 7c4aded5bb..e58b2eec3c 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -21,16 +21,20 @@ let coqc_main () = (* Careful because init_toplevel will call Summary.init_summaries, thus options such as `quiet` have to be set after the main initialisation is run. *) - let coqc_init ~opts args = + let coqc_init ~opts = set_noninteractive_mode (); - let opts, args = Coqtop.(coqtop_toplevel.init) ~opts args in - opts, args - in + Coqtop.(coqtop_toplevel.init) ~opts in + let custom_coqc = Coqtop.{ + coqtop_toplevel with + help = Usage.print_usage_coqc; + init = coqc_init; + parse_extra = (fun ~opts extras -> Coqcargs.parse extras, []); + } in let opts, extras = Topfmt.(in_phase ~phase:Initialization) - Coqtop.(init_batch_toplevel ~help:Usage.print_usage_coqc ~init:Coqargs.default coqc_init) List.(tl (Array.to_list Sys.argv)) in + Coqtop.(init_batch_toplevel ~help:Usage.print_usage_coqc ~init:Coqargs.default (fun ~opts extras -> coqc_init ~opts; (opts, extras))) List.(tl (Array.to_list Sys.argv)) in - let copts = Coqcargs.parse extras in + let copts, extras = custom_coqc.Coqtop.parse_extra ~opts extras in if not opts.Coqargs.config.Coqargs.glob_opt then Dumpglob.dump_to_dotglob (); diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 2f2cebe074..58dd994dcd 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -244,14 +244,16 @@ let init_toplevel ~help ~init custom_init arglist = Stm.init_core (); batch, opts, extras -type init_fn = opts:Coqargs.t -> string list -> Coqargs.t * string list - let init_batch_toplevel ~help ~init custom_init args = let run_mode, opts, extras = init_toplevel ~help ~init custom_init args in opts, extras -type custom_toplevel = - { init : init_fn +type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list + +type 'a custom_toplevel = + { parse_extra : 'a extra_args_fn + ; help : unit -> unit + ; init : opts:Coqargs.t -> unit ; run : opts:Coqargs.t -> state:Vernac.State.t -> unit ; opts : Coqargs.t } @@ -279,14 +281,18 @@ let init_toploop opts = let state = Ccompile.load_init_vernaculars opts ~state in state -let coqtop_init ~opts extra = +let coqtop_init ~opts = init_color opts.config; CoqworkmgrApi.(init !async_proofs_worker_priority); - Flags.if_verbose print_header (); - opts, extra + Flags.if_verbose print_header () + +let coqtop_parse_extra ~opts extras = + opts, extras let coqtop_toplevel = - { init = coqtop_init + { parse_extra = coqtop_parse_extra + ; help = Usage.print_usage_coqtop + ; init = coqtop_init ; run = Coqloop.loop ; opts = Coqargs.default } @@ -298,7 +304,7 @@ let start_coq custom = try let run_mode, opts, extras = init_toplevel - ~help:Usage.print_usage_coqtop ~init:default custom.init + ~help:Usage.print_usage_coqtop ~init:default (fun ~opts extras -> let opts, extras = custom.parse_extra ~opts extras in custom.init ~opts; (opts, extras)) (List.tl (Array.to_list Sys.argv)) in if not (CList.is_empty extras) then begin prerr_endline ("Don't know what to do with "^String.concat " " extras); diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index d1f0f78355..3f2d458407 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -13,24 +13,26 @@ [run] launches a custom toplevel. *) -type init_fn = opts:Coqargs.t -> string list -> Coqargs.t * string list +type 'a extra_args_fn = opts:Coqargs.t -> string list -> 'a * string list -type custom_toplevel = - { init : init_fn +type 'a custom_toplevel = + { parse_extra : 'a extra_args_fn + ; help : unit -> unit + ; init : opts:Coqargs.t -> unit ; run : opts:Coqargs.t -> state:Vernac.State.t -> unit ; opts : Coqargs.t } -(** [init_toplevel ~help ~init custom_init arg_list] - Common Coq initialization and argument parsing *) +(** [init_toplevel custom] + Customized Coq initialization and argument parsing *) val init_batch_toplevel : help:(unit -> unit) -> init:Coqargs.t - -> init_fn + -> Coqargs.t extra_args_fn -> string list -> Coqargs.t * string list -val coqtop_toplevel : custom_toplevel +val coqtop_toplevel : Coqargs.t custom_toplevel (** The Coq main module. [start custom] will parse the command line, print the banner, initialize the load path, load the input state, @@ -38,4 +40,4 @@ val coqtop_toplevel : custom_toplevel produce the output state if any, and finally will launch [custom.run]. *) -val start_coq : custom_toplevel -> unit +val start_coq : Coqargs.t custom_toplevel -> unit diff --git a/toplevel/workerLoop.ml b/toplevel/workerLoop.ml index d362f9db22..6d147ac308 100644 --- a/toplevel/workerLoop.ml +++ b/toplevel/workerLoop.ml @@ -13,18 +13,21 @@ let rec parse = function | x :: rest -> x :: parse rest | [] -> [] -let arg_init init ~opts extra_args = - let extra_args = parse extra_args in +let worker_parse_extra ~opts extra_args = + opts, parse extra_args + +let worker_init init ~opts = Flags.quiet := true; init (); - CoqworkmgrApi.(init !async_proofs_worker_priority); - opts, extra_args + CoqworkmgrApi.(init !async_proofs_worker_priority) let start ~init ~loop = let open Coqtop in let custom = { + parse_extra = worker_parse_extra; + help = (fun _ -> output_string stderr "Same options as coqtop"); opts = Coqargs.default; - init = arg_init init; + init = worker_init init; run = (fun ~opts:_ ~state:_ -> loop ()); } in start_coq custom |