diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 28 | ||||
| -rw-r--r-- | toplevel/coqtop.mli | 7 | ||||
| -rw-r--r-- | toplevel/usage.ml | 4 | ||||
| -rw-r--r-- | toplevel/usage.mli | 2 |
4 files changed, 15 insertions, 26 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index bc9f682623..864bf2e35b 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -151,12 +151,12 @@ let usage () = let warning s = msg_warning (str s) let ide_slave = ref false +let filter_opts = ref false -let ide_args = ref [] let parse_args arglist = let glob_opt = ref false in let rec parse = function - | [] -> () + | [] -> [] | "-with-geoproof" :: s :: rem -> if s = "yes" then Coq_config.with_geoproof := true else if s = "no" then Coq_config.with_geoproof := false @@ -255,15 +255,15 @@ let parse_args arglist = | "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem | "-coqlib" :: [] -> usage () - | "-where" :: _ -> print_endline (Envars.coqlib ()); exit 0 + | "-where" :: _ -> print_endline (Envars.coqlib ()); exit (if !filter_opts then 2 else 0) - | ("-config"|"--config") :: _ -> Usage.print_config (); exit 0 + | ("-config"|"--config") :: _ -> Usage.print_config (); exit (if !filter_opts then 2 else 0) | ("-quiet"|"-silent") :: rem -> Flags.make_silent true; parse rem | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () - | ("-v"|"--version") :: _ -> Usage.version () + | ("-v"|"--version") :: _ -> Usage.version (if !filter_opts then 2 else 0) | "-init-file" :: f :: rem -> set_rcfile f; parse rem | "-init-file" :: [] -> usage () @@ -291,9 +291,9 @@ let parse_args arglist = | "-ideslave" :: rem -> ide_slave := true; parse rem - | s :: rem -> - ide_args := s :: !ide_args; - parse rem + | "-filteropts" :: rem -> filter_opts := true; parse rem + + | s :: rem -> s :: (parse rem) in try parse arglist @@ -311,8 +311,10 @@ let init arglist = Lib.init(); begin try - parse_args arglist; - if !ide_args <> [] then usage (); + let foreign_args = parse_args arglist in + if !filter_opts then + (print_string (String.concat "\n" foreign_args); exit 0); + (* no else. ignore additional options. makes life easier *) if !ide_slave then begin Flags.make_silent true; Pfedit.set_undo (Some 5000); @@ -348,12 +350,6 @@ let init arglist = let init_toplevel = init -let init_ide arglist = - Flags.make_silent true; - Pfedit.set_undo (Some 5000); - Ide_blob.init_stdout (); - List.rev !ide_args - let start () = init_toplevel (List.tl (Array.to_list Sys.argv)); if !ide_slave then diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 2c55f6509c..9da66398c2 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -12,10 +12,3 @@ produce the output state if any, and finally will launch [Toplevel.loop]. *) val start : unit -> unit - -(** [init_ide] is to be used by the Coq IDE. - It does everything [start] does, except launching the toplevel loop. - It returns the list of Coq files given on the command line. *) - -val init_ide : System.physical_path list -> string list - diff --git a/toplevel/usage.ml b/toplevel/usage.ml index fc4d18b57d..34e8d0fb53 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -let version () = +let version ret = Printf.printf "The Coq Proof Assistant, version %s (%s)\n" Coq_config.version Coq_config.date; Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version; - exit 0 + exit ret (* print the usage of coqtop (or coqc) on channel co *) diff --git a/toplevel/usage.mli b/toplevel/usage.mli index aa59588e6d..0b98f061bd 100644 --- a/toplevel/usage.mli +++ b/toplevel/usage.mli @@ -8,7 +8,7 @@ (** {6 Prints the version number on the standard output and exits (with 0). } *) -val version : unit -> 'a +val version : int -> 'a (** {6 Prints the usage on the error output, preceeded by a user-provided message. } *) val print_usage : string -> unit |