This test stresses automatic insertion.

[helm.git] / helm / matita / matitaMathView.ml

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 <- [];