_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;
val model =
new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview
- val model_univs =
- new MatitaGtkMisc.multiStringListModel ~cols:2 win#universesTreeview
val mutable lastDir = "" (* last loaded "directory" *)
*
* 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
(* self#_showMath *)
method private egg () =
- win#mathOrListNotebook#goto_page 2;
+ self#_showEgg;
Lazy.force load_easter_egg
method private redraw_gviz ?center_on () =
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 =