From 55e646b795e4a7beedf1263ea734477bd4762931 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 28 Jul 2005 17:18:20 +0000 Subject: [PATCH] The logo is now showed in the sequents_viewer window when there is no proof in progress. --- helm/matita/matita.ml | 4 ++-- helm/matita/matita.txt | 2 +- helm/matita/matitaGuiTypes.mli | 2 ++ helm/matita/matitaMathView.ml | 15 +++++++++++++-- 4 files changed, 18 insertions(+), 5 deletions(-) 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 <- []; -- 2.39.2