Coqide is not built with coqmktop any more

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

4 files changed, 20 insertions, 28 deletions

diff --git a/Makefile.build b/Makefile.build
index e6227aea6..feb09fd57 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -245,7 +245,6 @@ scripts/tolink.ml: Makefile.build Makefile.common
 	$(HIDE)echo "let copts = \"-cclib -lcoqrun\"" > $@
 	$(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@
 	$(HIDE)echo "let core_objs = \""$(OBJSMOD)"\"" >> $@
-	$(HIDE)echo "let ide = \""$(IDEMOD)"\"" >> $@
 
 # coqc
 
@@ -308,14 +307,14 @@ coqide-byte: $(COQIDEBYTE) $(COQIDE)
 coqide-opt:  $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE)
 coqide-files: $(IDEFILES)
 
-$(COQIDEOPT): $(COQTOPOPT) $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) ide/ide.cmxa
-	$(SHOW)'COQMKTOP -o $@'	
-	$(HIDE)$(COQMKTOP) -boot -ide -opt $(OPTFLAGS) -o $@
+$(COQIDEOPT): $(LINKIDEOPT) $(LIBCOQRUN) $(COQTOPOPT)
+	$(SHOW)'OCAMLOPT -o $@'
+	$(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa gtkThread.cmx dynlink.cmxa str.cmxa $(CAMLP4MOD).cmxa $(LIBCOQRUN) $(LINKIDEOPT)
 	$(STRIP) $@
 
-$(COQIDEBYTE): $(COQTOPBYTE) $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) ide/ide.cma
-	$(SHOW)'COQMKTOP -o $@'	
-	$(HIDE)$(COQMKTOP) -boot -g -ide -top $(BYTEFLAGS) -o $@
+$(COQIDEBYTE): $(LINKIDE) $(LIBCOQRUN) $(COQTOPBYTE)
+	$(SHOW)'OCAMLOPT -o $@'
+	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma gtkThread.cmo dynlink.cma str.cma $(CAMLP4MOD).cma $(COQRUNBYTEFLAGS) $(LIBCOQRUN) $(LINKIDE)
 
 $(COQIDE):
 	cd bin; ln -sf coqide.$(HASCOQIDE)$(EXE) coqide$(EXE)
diff --git a/Makefile.common b/Makefile.common
index 95063aa2f..9e45758c4 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -29,6 +29,12 @@ CHICKENOPT:=bin/coqchk.opt$(EXE)
 BESTCHICKEN:=bin/coqchk.$(BEST)$(EXE)
 CHICKEN:=bin/coqchk$(EXE)
 
+ifeq ($(CAMLP4),camlp4)
+CAMLP4MOD:=camlp4lib
+else
+CAMLP4MOD:=gramlib
+endif
+
 ifneq ($(HASNATDYNLINK),false)
   DYNLINKCMXA:=dynlink.cmxa
   NATDYNLINKDEF:=-DHasDynlink
@@ -213,6 +219,9 @@ LINKCMX:=$(CONFIG:.cmo=.cmx) $(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)
 
 IDECMA:=ide/ide.cma
 
+LINKIDE:=$(LINKCMO) $(IDECMA) ide/coqide_main.ml
+LINKIDEOPT:=$(LINKCMX) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml
+
 # modules known by the toplevel of Coq
 
 OBJSMOD:=Coq_config $(shell cat $(CORECMA:.cma=.mllib))
diff --git a/ide/coqide_main.ml b/ide/coqide_main.ml
new file mode 100644
index 000000000..52c956c3c
--- /dev/null
+++ b/ide/coqide_main.ml
@@ -0,0 +1 @@
+let () = Coqide.start ()
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index d4a76b6cc..0ff487fb4 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -27,7 +27,6 @@ let split_list l = Str.split spaces l
 let copts     = split_list Tolink.copts
 let core_objs = split_list Tolink.core_objs
 let core_libs = split_list Tolink.core_libs
-let ide       = split_list Tolink.ide
 
 (* 3. Toplevel objects *)
 let camlp4topobjs =
@@ -51,12 +50,10 @@ let opt        = ref false
 let full       = ref false
 let top        = ref false
 let searchisos = ref false
-let coqide     = ref false
 let echo       = ref false
 
 let src_dirs () =
-  [ []; ["kernel";"byterun"]; [ "config" ]; [ "toplevel" ] ] @
-  if !coqide then [[ "ide" ]] else []
+  [ []; ["kernel";"byterun"]; [ "config" ]; [ "toplevel" ] ]
 
 let includes () =
   let coqlib = Envars.coqlib () in
@@ -65,8 +62,7 @@ let includes () =
       (fun d l -> "-I" :: ("\"" ^ List.fold_left Filename.concat coqlib d ^ "\"") :: l)
       (src_dirs ())
       (["-I"; "\"" ^ camlp4lib ^ "\""] @
-	 ["-I"; "\"" ^ coqlib ^ "\""] @
-	 (if !coqide then ["-thread"; "-I"; "+lablgtk2"] else []))
+	  ["-I"; "\"" ^ coqlib ^ "\""])
 
 (* Transform bytecode object file names in native object file names *)
 let native_suffix f =
@@ -92,18 +88,10 @@ let files_to_link userfiles =
     if not !opt || Coq_config.has_natdynlink then dynobjs else [] in
   let toplevel_objs =
     if !top then topobjs else if !opt then notopobjs else [] in
-  let ide_objs =
-    if !coqide then "Threads"::"Lablgtk"::"GtkThread"::ide else []
-  in
-  let ide_libs =
-    if !coqide then
-      ["threads.cma" ; "lablgtk.cma" ; "gtkThread.cmo" ; "ide/ide.cma" ]
-    else []
-  in
-  let objs = dyn_objs @ libobjs @ core_objs @ toplevel_objs @ ide_objs in
+  let objs = dyn_objs @ libobjs @ core_objs @ toplevel_objs in
   let modules = List.map module_of_file (objs @ userfiles)
   in
-  let libs = dyn_objs @ libobjs @ core_libs @ toplevel_objs @ ide_libs in
+  let libs = dyn_objs @ libobjs @ core_libs @ toplevel_objs in
   let libstolink =
     (if !opt then List.map native_suffix libs else libs) @ userfiles
   in
@@ -143,7 +131,6 @@ let usage () =
 \n  -o exec-file   Specify the name of the resulting toplevel\
 \n  -boot          Run in boot mode\
 \n  -echo          Print calls to external commands\
-\n  -ide           Build a toplevel for the Coq IDE\
 \n  -full          Link high level tactics\
 \n  -opt           Compile in native code\
 \n  -searchisos    Build a toplevel for SearchIsos\
@@ -169,8 +156,6 @@ let parse_args () =
     | "-opt" :: rem -> opt := true ; parse (op,fl) rem
     | "-full" :: rem -> full := true ; parse (op,fl) rem
     | "-top" :: rem -> top := true ; parse (op,fl) rem
-    | "-ide" :: rem ->
-        coqide := true; parse (op,fl) rem
     | "-v8" :: rem ->
 	Printf.eprintf "warning: option -v8 deprecated";
 	parse (op,fl) rem
@@ -257,8 +242,6 @@ let create_tmp_main_file modules =
     (* Start the right toplevel loop: Coq or Coq_searchisos *)
     if !searchisos then
       output_string oc "Cmd_searchisos_line.start();;\n"
-    else if !coqide then
-      output_string oc "Coqide.start();;\n"
     else
       output_string oc "Coqtop.start();;\n";
     close_out oc;