mise en place de why-ide

Makefile.in

@@ -89,7 +89,7 @@ BINARYL=bin/whyl.$(OCAMLBEST)
 
 TOOLS=bin/why-cpulimit
 
-all: .depend $(BINARY) $(BINARYL) $(TOOLS) apidoc
+all: .depend $(BINARY) $(BINARYL) $(TOOLS) apidoc why-ide-@LABLGTK2@
 
 # refrain parallel make (-j nn) from starting ocaml compilation too early 
 *.cm*: .depend
@@ -159,8 +159,10 @@ DRIVER_CMO := $(addprefix src/driver/,$(DRIVER_CMO))
 PRINTER_CMO := print_real.cmo alt_ergo.cmo why3.cmo smt.cmo coq.cmo
 PRINTER_CMO := $(addprefix src/printer/,$(PRINTER_CMO))
 
-CMO = $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(DRIVER_CMO)\
-      $(TRANSFORM_CMO) $(PRINTER_CMO) src/main.cmo
+LIBCMO = $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(DRIVER_CMO)\
+         $(TRANSFORM_CMO) $(PRINTER_CMO)
+
+CMO = $(LIBCMO) src/main.cmo
 CMX = $(CMO:.cmo=.cmx)
 
 bin/why.opt: $(CMX) 
@@ -246,26 +248,26 @@ bin/why-cpulimit: src/tools/@CPULIMIT@.c
 # graphical interface
 #####################
 
-GCMO = $(CMO) intf/colors.cmo intf/tags.cmo intf/tools.cmo intf/tagsplit.cmo\
-	      intf/astprinter.cmo intf/astnprinter.cmo intf/astpprinter.cmo\
-	      intf/model.cmo intf/cache.cmo intf/gConfig.cmo intf/hilight.cmo\
-	      intf/whyhilight.cmo intf/pprinter.cmo intf/preferences.cmo intf/stat.cmo
+IDE_CMO := ide_main.cmo
+IDE_CMO := $(addprefix src/ide/,$(IDE_CMO))
+
+GCMO = $(LIBCMO) $(IDE_CMO)
 GCMX = $(GCMO:.cmo=.cmx)
 
-gwhy-yes: bin/gwhy.$(OCAMLBEST)
-gwhy-no:
-gwhy: bin/gwhy.$(OCAMLBEST)
+why-ide-yes: bin/why-ide.$(OCAMLBEST)
+why-ide-no:
+why-ide: bin/why-ide.$(OCAMLBEST)
 
-bin/gwhy.opt: $(GCMX)
-	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ unix.cmxa threads.cmxa nums.cmxa str.cmxa graph.cmxa lablgtk.cmxa gtkThread.cmx $^
+bin/why-ide.opt: $(GCMX)
+	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ threads.cmxa nums.cmxa lablgtk.cmxa gtkThread.cmx $^
 	$(STRIP)    $@
 
-bin/gwhy.static: $(GCMX)
-	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLOPT) -cclib -static $(OFLAGS) -o $@ unix.cmxa threads.cmxa nums.cmxa str.cmxa graph.cmxa lablgtk.cmxa gtkThread.cmx $^
+bin/why-ide.static: $(GCMX)
+	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLOPT) -cclib -static $(OFLAGS) -o $@ threads.cmxa nums.cmxa lablgtk.cmxa gtkThread.cmx $^
 	$(STRIP)    $@
 
-bin/gwhy.byte: $(GCMO)
-	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLC) $(BFLAGS) -o $@ unix.cma str.cma nums.cma graph.cma lablgtk.cma threads.cma gtkThread.cmo $^
+bin/why-ide.byte: $(GCMO)
+	$(if $(QUIET),@echo 'Linking  $@' &&) $(OCAMLC) $(BFLAGS) -o $@ nums.cma lablgtk.cma threads.cma gtkThread.cmo $^
 
 # bench
 #######
@@ -300,15 +302,15 @@ bench_plugins:: $(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) $(BINARY) byte \
 
 install: install-binary install-lib install-man 
 
-BINARYFILES = $(BINARY) bin/gwhy.$(OCAMLBEST) 
+BINARYFILES = $(BINARY) bin/why-ide.$(OCAMLBEST) 
 
 # install-binary should not depend on $(BINARYFILES); otherwise it
-# enforces the compilation of gwhy, even when lablgtk2 is not installed
+# enforces the compilation of why-ide, even when lablgtk2 is not installed
 install-binary: 
 	mkdir -p $(BINDIR)
 	cp -f $(BINARY) $(BINDIR)/why$(EXE)
-	if test -f bin/gwhy.$(OCAMLBEST); then \
-		cp -f bin/gwhy.$(OCAMLBEST) $(BINDIR)/gwhy-bin$(EXE); \
+	if test -f bin/why-ide.$(OCAMLBEST); then \
+		cp -f bin/why-ide.$(OCAMLBEST) $(BINDIR)/why-ide-bin$(EXE); \
 	fi
 
 install-lib: 
@@ -351,13 +353,13 @@ install-mizar-yes:
 	cp lib/mizar/why.miz @MIZARLIB@/mml
 	cp lib/mizar/dict/why.voc @MIZARLIB@/mml/dict
 
-local-install: $(BINARY) $(WHYCONFIG) $(CADUCEUS) $(JESSIE) bin/gwhy.$(OCAMLBEST) byte bin/gwhy.byte 
+local-install: $(BINARY) $(WHYCONFIG) $(CADUCEUS) $(JESSIE) bin/why-ide.$(OCAMLBEST) byte bin/why-ide.byte 
 	cp $(BINARY) $$HOME/bin/why
 	cp $(WHYCONFIG) $$HOME/bin/why
 	cp $(CADUCEUS) $$HOME/bin/caduceus
 	cp $(JESSIE) $$HOME/bin/jessie
-	if test -f bin/gwhy.$(OCAMLBEST); then \
-	  cp -f bin/gwhy.$(OCAMLBEST) $$HOME/bin/gwhy; \
+	if test -f bin/why-ide.$(OCAMLBEST); then \
+	  cp -f bin/why-ide.$(OCAMLBEST) $$HOME/bin/why-ide; \
 	fi
 
 local: install
@@ -550,7 +552,7 @@ WWW = /users/www-perso/projets/why
 FTP = $(WWW)/download
 WWWKRAKATOA = /users/www-perso/projets/krakatoa
 
-FILES =src/*.ml* c/*.ml* jc/*.ml* java/*.ml* ml/*.ml* ml/*/*.ml* intf/*.ml* tools/*.ml* tools/*.c bin/gwhy.sh \
+FILES =src/*.ml* c/*.ml* jc/*.ml* java/*.ml* ml/*.ml* ml/*/*.ml* intf/*.ml* tools/*.ml* tools/*.c bin/why-ide.sh \
        mix/*.ml* \
        version.sh Version Makefile.in configure.in configure .depend .depend.coq \
        config/check_ocamlgraph.ml \

configure.in

@@ -260,6 +260,7 @@ dnl fi
 # checking for lablgtk2
 AC_CHECK_FILE($OCAMLLIB/lablgtk2/lablgtk.cma,LABLGTK2=yes,LABLGTK2=no)
 # AC_CHECK_PROG(LABLGTK2,lablgtk2,yes,no) not always available (Win32)
+# TODO: check gtksourceview
 if test "$LABLGTK2" = yes ; then
       INCLUDEGTK2="-I +lablgtk2"
 fi

src/ide/ide_main.ml

+
+let () = ignore (GtkMain.Main.init ())
+
+(* config *)
+let window_width = 1024
+let window_height = 768
+
+let font_size = ref 10
+let font_family = "Monospace"
+
+
+let main () =
+  let w = GWindow.window 
+    ~allow_grow:true ~allow_shrink:true
+    ~width:window_width ~height:window_height 
+    ~title:"why-ide" ()
+  in
+  let _ = w#connect#destroy ~callback:(fun () -> exit 0) in
+  let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in
+
+  (* Menu *)
+  let menubar = GMenu.menu_bar ~packing:vbox#pack () in
+  let factory = new GMenu.factory menubar in
+  let accel_group = factory#accel_group in
+  let file_menu = factory#add_submenu "_File" in
+  let file_factory = new GMenu.factory file_menu ~accel_group in
+  let _ = 
+    file_factory#add_image_item ~key:GdkKeysyms._Q ~label:"_Quit" 
+      ~callback:(fun () -> exit 0) () 
+  in
+
+  (* top line *)
+  let top_box = GPack.hbox ~packing:vbox#pack () in
+  (* le bouton Replay *)
+  let button = 
+    GButton.button ~label:"repousser le front d'obsolescence" 
+    ~packing:top_box#add ()
+  in
+  ignore (button#connect#clicked
+	    (fun () -> Format.printf "Andrei, tu es trop fort !@."));
+
+
+  w#add_accel_group accel_group;
+  w#show ()
+
+let () =
+  main ();
+  GtkThread.main ()
+
+(*
+Local Variables: 
+compile-command: "unset LANG; make -C ../.. why-ide-yes"
+End: 
+*)