CoqIDE argv parsing delegated to coqtop

Introduces some hacks to have a consistent user experience. When coqtop
prints info on self then exit, return code is 2 if called with
-filteropts, 0 else
For now, no options are accepted by coqide. there is no way for now to
specify a filename that begins with a dash.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13415 85f007b7-540e-0410-9357-904b9bb8a0f7

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