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 610f22a4ec7943d6b3b53e7117fb10e9b5b1958b..72dff80581b73e641240e364384684bab9f1c37a 100644 (file)
--- 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 406ecc63a858b532affa01cf225e7e544430574f..701b27ebb0417ef1b6b74409f4f47e1288404376 100644 (file)
--- 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 d9c2ece2a35c922675d0f88431b439b6e3b1ac21..963bb4698a4ec80a48df645efd83b71c31949d50 100644 (file)
--- 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 ca82df075d4387d648c4bb760d1a41dbcdecceea..13035b02b5ca8be6e57ab626f7551796fabf0728 100644 (file)
--- 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 <- [];