diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/ccompile.ml | 5 | ||||
| -rw-r--r-- | toplevel/ccompile.mli | 4 | ||||
| -rw-r--r-- | toplevel/coqc.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqcargs.ml | 27 | ||||
| -rw-r--r-- | toplevel/coqcargs.mli | 2 |
5 files changed, 20 insertions, 20 deletions
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index ca09bad441..041097d2d3 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -216,9 +216,8 @@ let compile_file opts stm_opts copts injections (f_in, echo) = else compile opts stm_opts copts injections ~echo ~f_in ~f_out -let compile_files (opts, stm_opts) copts injections = - let compile_list = copts.compile_list in - List.iter (compile_file opts stm_opts copts injections) compile_list +let compile_file opts stm_opts copts injections = + Option.iter (compile_file opts stm_opts copts injections) copts.compile_file (******************************************************************************) (* VIO Dispatching *) diff --git a/toplevel/ccompile.mli b/toplevel/ccompile.mli index 9f3783f32e..e9e83af3ad 100644 --- a/toplevel/ccompile.mli +++ b/toplevel/ccompile.mli @@ -12,8 +12,8 @@ the init (rc) file *) val load_init_vernaculars : Coqargs.t -> state:Vernac.State.t-> Vernac.State.t -(** [compile_files opts] compile files specified in [opts] *) -val compile_files : Coqargs.t * Stm.AsyncOpts.stm_opt -> Coqcargs.t -> Coqargs.injection_command list -> unit +(** [compile_file opts] compile file specified in [opts] *) +val compile_file : Coqargs.t -> Stm.AsyncOpts.stm_opt -> Coqcargs.t -> Coqargs.injection_command list -> unit (** [do_vio opts] process [.vio] files in [opts] *) val do_vio : Coqargs.t -> Coqcargs.t -> Coqargs.injection_command list -> unit diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index a403640149..b7af66b2ee 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -44,7 +44,7 @@ coqc specific options:\ let coqc_main ((copts,_),stm_opts) injections ~opts = Topfmt.(in_phase ~phase:CompilationPhase) - Ccompile.compile_files (opts,stm_opts) copts injections; + Ccompile.compile_file opts stm_opts copts injections; (* Careful this will modify the load-path and state so after this point some stuff may not be safe anymore. *) diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml index f84d73ed17..efd8a79e18 100644 --- a/toplevel/coqcargs.ml +++ b/toplevel/coqcargs.ml @@ -13,7 +13,7 @@ type compilation_mode = BuildVo | BuildVio | Vio2Vo | BuildVos | BuildVok type t = { compilation_mode : compilation_mode - ; compile_list: (string * bool) list (* bool is verbosity *) + ; compile_file: (string * bool) option (* bool is verbosity *) ; compilation_output_name : string option ; vio_checking : bool @@ -32,7 +32,7 @@ type t = let default = { compilation_mode = BuildVo - ; compile_list = [] + ; compile_file = None ; compilation_output_name = None ; vio_checking = false @@ -62,17 +62,13 @@ let error_missing_arg s = prerr_endline "See -help for the syntax of supported options"; exit 1 -let check_compilation_output_name_consistency args = - match args.compilation_output_name, args.compile_list with - | Some _, _::_::_ -> - prerr_endline ("Error: option -o is not valid when more than one"); - prerr_endline ("file have to be compiled") - | _ -> () +let arg_error msg = CErrors.user_err msg let is_dash_argument s = String.length s > 0 && s.[0] = '-' let add_compile ?echo copts s = - if is_dash_argument s then (prerr_endline ("Unknown option " ^ s); exit 1); + if is_dash_argument s then + arg_error Pp.(str "Unknown option " ++ str s); (* make the file name explicit; needed not to break up Coq loadpath stuff. *) let echo = Option.default copts.echo echo in let s = @@ -81,7 +77,14 @@ let add_compile ?echo copts s = then concat current_dir_name s else s in - { copts with compile_list = (s,echo) :: copts.compile_list } + { copts with compile_file = Some (s,echo) } + +let add_compile ?echo copts v_file = + match copts.compile_file with + | Some _ -> + arg_error Pp.(str "More than one file to compile: " ++ str v_file) + | None -> + add_compile ?echo copts v_file let add_vio_task opts f = { opts with vio_tasks = f :: opts.vio_tasks } @@ -230,14 +233,12 @@ let parse arglist : t = try let opts, extra = parse default in let args = List.fold_left add_compile opts extra in - check_compilation_output_name_consistency args; args with any -> fatal_error any let parse args = let opts = parse args in { opts with - compile_list = List.rev opts.compile_list - ; vio_tasks = List.rev opts.vio_tasks + vio_tasks = List.rev opts.vio_tasks ; vio_files = List.rev opts.vio_files } diff --git a/toplevel/coqcargs.mli b/toplevel/coqcargs.mli index 905250e363..96895568ea 100644 --- a/toplevel/coqcargs.mli +++ b/toplevel/coqcargs.mli @@ -27,7 +27,7 @@ type compilation_mode = BuildVo | BuildVio | Vio2Vo | BuildVos | BuildVok type t = { compilation_mode : compilation_mode - ; compile_list: (string * bool) list (* bool is verbosity *) + ; compile_file: (string * bool) option (* bool is verbosity *) ; compilation_output_name : string option ; vio_checking : bool |