X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2FmatitaMathView.ml;h=a8f20aa1863c5765565618f87b8a68ace7b892dd;hb=53452958508001e7af3090695b619fe92135fb9e;hp=4b7b376b417933ad23d3e3f76cf47792e571f303;hpb=cd664aefb80554952ed9b010f0c5199ce3a6f8f2;p=helm.git diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index 4b7b376b4..a8f20aa18 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -727,8 +727,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = _metasenv <- `Old []; self#script#setGoal None - method nload_sequents : 'status. #NTacStatus.tac_status as 'status -> unit - = fun (status : #NTacStatus.tac_status) -> + method nload_sequents : 'status. #GrafiteTypes.status as 'status -> unit + = fun (status : #GrafiteTypes.status) -> let _,_,metasenv,subst,_ = status#obj in _metasenv <- `New (metasenv,subst); pages <- 0; @@ -1052,8 +1052,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) val model = new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview - val model_univs = - new MatitaGtkMisc.multiStringListModel ~cols:2 win#universesTreeview val mutable lastDir = "" (* last loaded "directory" *) @@ -1093,11 +1091,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) * * Use only these functions to switch between the tabs *) - method private _showMath = win#mathOrListNotebook#goto_page 0 - method private _showList = win#mathOrListNotebook#goto_page 1 - method private _showList2 = win#mathOrListNotebook#goto_page 5 - method private _showSearch = win#mathOrListNotebook#goto_page 6 - method private _showGviz = win#mathOrListNotebook#goto_page 3 + method private _showMath = win#mathOrListNotebook#goto_page 0 + method private _showList = win#mathOrListNotebook#goto_page 1 + method private _showEgg = win#mathOrListNotebook#goto_page 2 + method private _showGviz = win#mathOrListNotebook#goto_page 3 + method private _showSearch = win#mathOrListNotebook#goto_page 4 method private back () = try @@ -1142,7 +1140,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) (* self#_showMath *) method private egg () = - win#mathOrListNotebook#goto_page 2; + self#_showEgg; Lazy.force load_easter_egg method private redraw_gviz ?center_on () = @@ -1269,11 +1267,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) List.iter (fun (tag, s) -> model#easy_append ~tag s) l; self#_showList - method private _loadList2 l = - model_univs#list_store#clear (); - List.iter model_univs#easy_mappend l; - self#_showList2 - (** { public methods, all must call _load!! } *) method load entry =