From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 28 Jul 2005 17:18:20 +0000 (+0000)
Subject: The logo is now showed in the sequents_viewer window when there is no proof
X-Git-Tag: V_0_7_2~7
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=55e646b795e4a7beedf1263ea734477bd4762931;p=helm.git

The logo is now showed in the sequents_viewer window when there is no proof
in progress.
---

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 610f22a4e..72dff8058 100644
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -93,9 +93,9 @@ let _ =
         sequents_viewer#load_sequents status;
         sequents_viewer#goto_sequent goal
     | Proof proof -> 
-        prerr_endline "sequents_viewer#load_logo_with_qed (no proof)"; ()
+        sequents_viewer#load_logo_with_qed
     | No_proof -> 
-        prerr_endline "sequents_viewer#load_logo (no proof)"; ()
+        sequents_viewer#load_logo
     | Intermediate _ -> 
         assert false (* only the engine may be in this state *)
   in
diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 406ecc63a..701b27ebb 100644
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -49,7 +49,6 @@ TODO
   - keybinding globali: CTRL-{su,giu,...} devono fungere anche quando altre
     finestre hanno il focus (e.g. cicBrowser). C'e' gia' da qualche parte il
     codice che aggiunge i keybinding a tutte le eventBox, e' da ripristinare
-  - integrare il famoso logo mancante (anche nell'About dialog)
   - la finestrella per i development ha i pulsanti non sensitive.
     E' possibile fare "Build" senza selezionare nulla, ottenendo un
     assert false
@@ -97,6 +96,7 @@ TODO
   - non chiudere transitivamente i moo ?? 
 
 DONE
+- integrare il famoso logo mancante (anche nell'About dialog) -> CSC
 - invertibilita' dell'inserimento automatico di alias: quando si torna
   su bisognerebbe tornare su di un passo e non fare undo degli alias
   (Zack: nella history ci sono anche gli offset per sapere a che pezzo di
diff --git a/helm/matita/matitaGuiTypes.mli b/helm/matita/matitaGuiTypes.mli
index d9c2ece2a..963bb4698 100644
--- a/helm/matita/matitaGuiTypes.mli
+++ b/helm/matita/matitaGuiTypes.mli
@@ -115,6 +115,8 @@ end
 class type sequentsViewer =
 object
   method reset: unit
+  method load_logo: unit
+  method load_logo_with_qed: unit
   method load_sequents: ProofEngineTypes.status -> unit
   method goto_sequent: int -> unit  (* to be called _after_ load_sequents *)
 end
diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index ca82df075..13035b02b 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -388,7 +388,17 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
     val mutable goal2win = []   (* associative list: goal no -> scrolled win *)
     val mutable _metasenv = []
     val mutable scrolledWin: GBin.scrolled_window option = None
-      (* scrolled window to which cicMathView is currently attached *)
+      (* scrolled window to which the sequentViewer is currently attached *)
+    val logo = (GMisc.image ~file:"logo/matita_medium.png" () :> GObj.widget)
+    val logo_with_qed = (GMisc.image ~file:"logo/matita_small.png" () :> GObj.widget)
+
+    method load_logo =
+     notebook#set_show_tabs false;
+     notebook#append_page logo
+
+    method load_logo_with_qed =
+     notebook#set_show_tabs false;
+     notebook#append_page logo_with_qed
 
     method private tab_label metano =
       (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce
@@ -401,7 +411,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
           w#remove cicMathView#coerce;
           scrolledWin <- None
       | None -> ());
-      for i = 1 to pages do notebook#remove_page 0 done;
+      for i = 0 to pages do notebook#remove_page 0 done;
+      notebook#set_show_tabs true;
       pages <- 0;
       page2goal <- [];
       goal2page <- [];