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

8 files changed, 46 insertions, 33 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 78b1060ed7..c114e2c463 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -83,6 +83,23 @@ let version () =
     (if Mltop.is_native then "native" else "bytecode")
     (if Coq_config.best="opt" then "native" else "bytecode")
 
+let filter_coq_opts argv =
+  let prog = Sys.executable_name in
+  let dir = Filename.dirname prog in
+  let argstr = String.concat " " argv in
+  let oc,ic,ec = Unix.open_process_full (dir^"/coqtop.opt -filteropts "^argstr) (Unix.environment ()) in
+  let rec read_all_lines in_chan =
+    try
+      let arg = input_line in_chan in
+        arg::(read_all_lines in_chan)
+    with End_of_file -> [] in
+  let filtered_argv = read_all_lines oc in
+  let message = read_all_lines ec in
+  match Unix.close_process_full (oc,ic,ec) with
+    | Unix.WEXITED 0 -> true,filtered_argv
+    | Unix.WEXITED 2 -> false,filtered_argv
+    | _ -> false,message
+
 let eval_call coqtop (c:'a Ide_blob.call) =
   Safe_marshal.send coqtop.cin c;
   (Safe_marshal.receive: in_channel -> 'a Ide_blob.value) coqtop.cout
diff --git a/ide/coq.mli b/ide/coq.mli
index 8554a77574..a6928eaba8 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -14,6 +14,7 @@ open Ide_blob
 
 val short_version : unit -> string
 val version : unit -> string
+val filter_coq_opts : string list -> bool * string list
 
 type coqtop
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index a060104c30..45eddc84a0 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -3080,13 +3080,20 @@ let rec check_for_geoproof_input () =
 	(* cb_Dr#set_text "Ack" *)
     done
 
-let rec init = function
-  | [] -> []
-  | "-args"::str::rem -> sup_args := str; init rem
-  | f::rem -> f::(init rem)
+let process_argv argv =
+  try 
+    let continue,filtered = filter_coq_opts (List.tl argv) in
+    if not continue then
+      (List.iter Pervasives.prerr_endline filtered; exit 0);
+    if List.exists (fun arg -> String.get arg 0 == '-') filtered then
+      (output_string stderr "illegal coqide option\n"; exit 1);
+    filtered
+  with _ ->
+    (output_string stderr "coqtop choked on one of your option"; exit 1)
 
 let start () =
-  let files = init (List.tl (Array.to_list Sys.argv)) in
+  sup_args := String.concat " " (List.tl (Array.to_list Sys.argv));
+  let files = process_argv (Array.to_list Sys.argv) in
     ignore_break ();
     GtkMain.Rc.add_default_file (lib_ide_file ".coqide-gtk2rc");
     (try
@@ -3115,4 +3122,3 @@ let start () =
 	    crash_save 127
     done
 
-
diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index 1d5ba7f118..eb33850a7b 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -163,7 +163,7 @@ let parse_args () =
     | ("-config" | "--config") :: _ -> Usage.print_config (); exit 0
 
     | ("-v"|"--version") :: _ ->
-        Usage.version ()
+        Usage.version 0
     | f :: rem ->
 	if Sys.file_exists f then
 	  parse (f::cfiles,args) rem
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