From 6a95dc4210f723062df04a40b1ec1f2d0636e966 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Claude=20March=C3=A9?= <Claude.Marche@inria.fr>
Date: Mon, 4 Jun 2012 22:10:21 +0200
Subject: [PATCH] Alternative icons: installation, legend

---
 Makefile.in        |  8 +++++++-
 src/ide/gconfig.ml | 12 ++++++++++--
 2 files changed, 17 insertions(+), 3 deletions(-)

diff --git a/Makefile.in b/Makefile.in
index d9d17f7ae6..9693c6e1d3 100644
--- a/Makefile.in
+++ b/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?
diff --git a/src/ide/gconfig.ml b/src/ide/gconfig.ml
index 1905116c9e..432a016a3b 100644
--- a/src/ide/gconfig.ml
+++ b/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;
-- 
GitLab