Alternative icons: installation, legend

Makefile.in

@@ -213,6 +213,8 @@ clean::
 install_no_local::
 	mkdir -p $(BINDIR)
 	mkdir -p $(DATADIR)/why3/images
+	mkdir -p $(DATADIR)/why3/images/boomy
+	mkdir -p $(DATADIR)/why3/images/fatcow
 	mkdir -p $(DATADIR)/why3/emacs
 	mkdir -p $(DATADIR)/why3/lang
 	mkdir -p $(DATADIR)/why3/theories
@@ -222,7 +224,10 @@ install_no_local::
 	cp -f modules/*.mlw $(DATADIR)/why3/modules
 	cp -f drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
 	cp -f share/provers-detection-data.conf $(DATADIR)/why3/
+	cp -f share/images/icons.rc $(DATADIR)/why3/images
 	cp -f share/images/*.png $(DATADIR)/why3/images
+	cp -f share/images/boomy/*.png $(DATADIR)/why3/images/boomy
+	cp -f share/images/fatcow/*.png $(DATADIR)/why3/images/fatcow
 	cp -f share/why3session.dtd $(DATADIR)/why3
 	cp -rf share/javascript $(DATADIR)/why3/javascript
 	cp -f share/emacs/why.el $(DATADIR)/why3/emacs/why.el
@@ -1319,7 +1324,8 @@ DISTRIB_FILES = Version Makefile.in configure.in META.in configure \
       share/javascript/themes/default/*.gif \
       share/javascript/themes/default/*.png \
       share/javascript/themes/default/*.css \
-      share/emacs/why.el share/images/*.png share/lang/*.lang \
+      share/emacs/why.el share/lang/*.lang \
+      share/images/icons.rc share/images/*.png share/images/*/*.png \
       share/bash/why3 share/zsh/_why3 share/vim/why3.vim
 
 # TODO?

src/ide/gconfig.ml

@@ -495,16 +495,16 @@ let show_legend_window () =
   ib image_transf;
   i "   Transformation\n";
   it "Status column\n";
+  ib image_undone;
+  i "   External proof attempt not done\n";
   ib image_scheduled;
   i "   Scheduled external proof attempt\n";
   ib image_running;
   i "   Running external proof attempt\n";
   ib image_valid;
   i "   Goal is proved / Theory is fully verified\n";
-(*
   ib image_invalid;
   i "   External prover disproved the goal\n";
-*)
   ib image_timeout;
   i "   External prover reached the time limit\n";
   ib image_outofmemory;
@@ -513,6 +513,14 @@ let show_legend_window () =
   i "   External prover answer not conclusive\n";
   ib image_failure;
   i "   External prover call failed\n";
+  ib image_valid_obs;
+  i "   Valid but obsolete result\n";
+  ib image_unknown_obs;
+  i "   Answer not conclusive and obsolete\n";
+  ib image_invalid_obs;
+  i "   Prover disproved goal, but obsolete\n";
+  ib image_failure_obs;
+  i "   External prover call failed, obsolete\n";
   dialog#add_button "Close" `CLOSE ;
   let t = b#create_tag [`LEFT_MARGIN 10; `RIGHT_MARGIN 10 ] in
   b#apply_tag t ~start:b#start_iter ~stop:b#end_iter;