- added support for -debug, which avoid catching top level exceptions (still useless...

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

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 47f8c5a5c13d33320deb010b7a81df0187d6d285..43547b8ff9e835da80e588d3c1efdd8db659c1bb 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -404,11 +404,11 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
     val mutable scrolledWin: GBin.scrolled_window option = None
       (* scrolled window to which the sequentViewer is currently attached *)
     val logo = (GMisc.image
-      ~file:(BuildTimeConf.runtime_base_dir ^ "/logo/matita_medium.png") ()
+      ~file:(MatitaMisc.image_path "matita_medium.png") ()
       :> GObj.widget)
             
     val logo_with_qed = (GMisc.image
-      ~file:(BuildTimeConf.runtime_base_dir ^ "/logo/matita_small.png") ()
+      ~file:(MatitaMisc.image_path "matita_small.png") ()
       :> GObj.widget)
 
     method load_logo =
@@ -430,19 +430,19 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
           w#remove cicMathView#coerce;
           scrolledWin <- None
       | None -> ());
-      for i = 0 to pages do notebook#remove_page 0 done;
+      (match switch_page_callback with
+      | Some id ->
+          GtkSignal.disconnect notebook#as_widget id;
+          switch_page_callback <- None
+      | None -> ());
+      for i = 0 to pages do notebook#remove_page 0 done; 
       notebook#set_show_tabs true;
       pages <- 0;
       page2goal <- [];
       goal2page <- [];
       goal2win <- [];
-      _metasenv <- [];
+      _metasenv <- []; 
       self#script#setGoal ~-1;
-      (match switch_page_callback with
-      | Some id ->
-          GtkSignal.disconnect notebook#as_widget id;
-          switch_page_callback <- None
-      | None -> ())
 
     method load_sequents (status: ProofEngineTypes.status) =
       let ((_, metasenv, _, _), goal) = status in
@@ -593,6 +593,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     with exn -> fail (MatitaExcPp.to_string exn)
   in
   let handle_error' f = (fun () -> handle_error (fun () -> f ())) in
+  let load_easter_egg = lazy (
+    win#easterEggImage#set_file (MatitaMisc.image_path "meegg.png"))
+  in
   object (self)
     inherit scriptAccessor
     
@@ -682,9 +685,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
      * 
      * Use only these functions to switch between the tabs
      *)
-    method private _showList = win#mathOrListNotebook#goto_page 1
     method private _showMath = win#mathOrListNotebook#goto_page 0
-    
+    method private _showList = win#mathOrListNotebook#goto_page 1
+
     method private back () =
       try
         self#_load (self#_historyPrev ())
@@ -704,7 +707,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           (match entry with
           | `About `Current_proof -> self#home ()
           | `About `Blank -> self#blank ()
-          | `About `Us -> () (* TODO implement easter egg here :-] *)
+          | `About `Us -> self#egg ()
           | `Check term -> self#_loadCheck term
           | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
           | `Dir dir -> self#_loadDir dir
@@ -725,6 +728,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       failwith "not implemented _loadCheck";
       self#_showMath
 
+    method private egg () =
+      win#mathOrListNotebook#goto_page 2;
+      Lazy.force load_easter_egg
+
     method private home () =
       self#_showMath;
       match self#script#status.proof_status with