fichiers sur la ligne de commande passes a Coq IDE

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

4 files changed, 19 insertions, 12 deletions

diff --git a/Makefile b/Makefile
index 65233c85cc..16e942ffd8 100644
--- a/Makefile
+++ b/Makefile
@@ -455,7 +455,7 @@ beforedepend:: ide/config_lexer.ml ide/find_phrase.ml ide/highlight.ml
 FULLIDELIB=$(FULLCOQLIB)/ide
 IDEFILES=ide/coq.gif ide/.coqiderc
 
-ide: $(COQIDE)
+ide: $(COQIDE) states
 
 $(COQIDEOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) $(COQIDECMX)
 	$(COQMKTOP) -ide -opt $(COQIDEFLAGS) lablgtk.cmxa $(OPTFLAGS) -o $@ $(COQIDECMX)
diff --git a/ide/coq.ml b/ide/coq.ml
index 3a6b729ce1..65dfd99eb0 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -24,7 +24,7 @@ let msg x =
  
 let init () = 
   Options.make_silent true;
-  Coqtop.init ()
+  ignore (Coqtop.init_ide ())
 
 let i = ref 0
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 267174ad29..90c2c8eb72 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -112,7 +112,8 @@ let usage () =
 
 let warning s = msg_warning (str s)
 
-let parse_args () =
+let ide_args = ref []
+let parse_args is_ide =
   let rec parse = function
     | [] -> ()
 
@@ -200,8 +201,12 @@ let parse_args () =
 
     | "-v8" :: rem -> Options.v7 := false; parse rem
 
-    | s :: _ -> prerr_endline ("Don't know what to do with " ^ s); usage ()
-
+    | s :: _ -> 
+	if is_ide && Filename.check_suffix s ".v" then
+	  ide_args := s :: !ide_args
+	else begin
+	  prerr_endline ("Don't know what to do with " ^ s); usage ()
+	end
   in
   try
     parse (List.tl (Array.to_list Sys.argv))
@@ -218,13 +223,13 @@ let parse_args () =
 (* To prevent from doing the initialization twice *)
 let initialized = ref false
 
-let init () =
+let init is_ide =
   if not !initialized then begin
     initialized := true;
     Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
     Lib.init();
     try
-      parse_args ();
+      parse_args is_ide;
       re_exec ();
       if_verbose print_header ();
       init_load_path ();
@@ -245,8 +250,10 @@ let init () =
   if !batch_mode then (flush_all(); Profile.print_profile (); exit 0);
   Lib.declare_initial_state ()
 
+let init_ide () = init true; !ide_args
+
 let start () =
-  init ();
+  init false;
   Toplevel.loop();
   (* Initialise and launch the Ocaml toplevel *)
   Coqinit.init_ocaml_path();
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 42618505f7..1df5bb8c81 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -15,9 +15,9 @@
 
 val start : unit -> unit
 
-(* [init] is already called by [start], but exported here to be reused 
-   by the Coq IDE. It does everything [start] does, except launching
-   the toplevel loop. *)
+(* [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 : unit -> unit
+val init_ide : unit -> string list