added -args option to coqide to pass options to coqtops

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

3 files changed, 15 insertions, 12 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index fecd3f292..cb9d5b895 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -28,11 +28,13 @@ open Compat
 type coqtop = {
   mutable cout : in_channel ;
   mutable cin : out_channel ;
+  sup_args : string ;
 }
 
 let dummy_coqtop = {
   cout = stdin ;
   cin = stdout ;
+  sup_args = "" ;
 }
 
 let prerr_endline s = if !debug then prerr_endline s else ()
@@ -47,9 +49,6 @@ let msg m =
 let msgnl m =
   (msg m)^"\n"
 
-let init () = List.tl (Array.to_list Sys.argv)
-(*  Coqtop.init_ide (List.tl (Array.to_list Sys.argv))*)
-
 let i = ref 0
 
 let get_version_date () =
@@ -103,17 +102,17 @@ let rewind coqtop i = eval_call coqtop (Ide_blob.rewind i)
  
 let read_stdout coqtop = eval_call coqtop Ide_blob.read_stdout
 
-let spawn_coqtop () =
+let spawn_coqtop sup_args =
   let prog = Sys.argv.(0) in
   let dir = Filename.dirname prog in
-  let oc,ic = Unix.open_process (dir^"/coqtop.opt -ideslave") in
-  { cin = ic; cout = oc }
+  let oc,ic = Unix.open_process (dir^"/coqtop.opt -ideslave "^sup_args) in
+  { cin = ic; cout = oc ; sup_args = sup_args }
 
 let kill_coqtop coqtop = raw_interp coqtop "Quit."
 
 let reset_coqtop coqtop =
   kill_coqtop coqtop;
-  let ni = spawn_coqtop () in
+  let ni = spawn_coqtop coqtop.sup_args in
   coqtop.cin <- ni.cin;
   coqtop.cout <- ni.cout
 
diff --git a/ide/coq.mli b/ide/coq.mli
index 914eb708a..926919f70 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -19,7 +19,7 @@ type coqtop
 
 val dummy_coqtop : coqtop
 
-val spawn_coqtop : unit -> coqtop
+val spawn_coqtop : string -> coqtop
 
 val kill_coqtop : coqtop -> unit
 
@@ -43,8 +43,6 @@ end
 
 val reset_initial : unit -> unit
 
-val init : unit -> string list
-
 val raw_interp : coqtop -> string -> unit
 
 val interp : coqtop -> bool -> string -> int
diff --git a/ide/coqide.ml b/ide/coqide.ml
index e8198ec6f..4266d6fb3 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -529,6 +529,8 @@ let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) =
     buffer#apply_tag ~start:decl_start ~stop:decl_end Tags.Script.folded;
     buffer#apply_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden)
 
+let sup_args = ref ""
+
 class analyzed_view (_script:Undo.undoable_view) (_pv:GText.view) (_mv:GText.view) _cs _ct =
 object(self)
   val input_view = _script
@@ -1361,7 +1363,7 @@ let create_session () =
   let stack =
     Stack.create () in
   let ct =
-    spawn_coqtop () in
+    spawn_coqtop !sup_args in
   let legacy_av =
     new analyzed_view script proof message stack ct in
   let _ =
@@ -3117,9 +3119,13 @@ 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 start () =
-  let files = Coq.init () in
+  let files = init (List.tl (Array.to_list Sys.argv)) in
     ignore_break ();
     GtkMain.Rc.add_default_file (lib_ide_file ".coqide-gtk2rc");
     (try