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

3 files changed, 30 insertions, 6 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
 
-