X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=43547b8ff9e835da80e588d3c1efdd8db659c1bb;hb=1946ca7a51df0acb35d8e2ea001d194f1d2ccb12;hp=47f8c5a5c13d33320deb010b7a81df0187d6d285;hpb=33dd8006a7e0eb9c6c2a93b4d98c8ef88d2d49d1;p=helm.git diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 47f8c5a5c..43547b8ff 100644 --- 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