_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;
let my_id = Oo.id self in
cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers;
win#toplevel#misc#hide(); win#toplevel#destroy ());
- (* remove hbugs *)
- (*
- connect_menu_item win#hBugsTutorsMenuItem (fun () ->
- self#load (`HBugs `Tutors));
- *)
- win#hBugsTutorsMenuItem#misc#hide ();
connect_menu_item win#browserUrlMenuItem (fun () ->
win#browserUri#misc#grab_focus ());
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 _showHBugs = win#mathOrListNotebook#goto_page 4
+ 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
| `NCic (term, ctx, metasenv, subst) ->
self#_loadTermNCic term metasenv subst ctx
| `Dir dir -> self#_loadDir dir
- | `HBugs `Tutors -> self#_loadHBugsTutors
| `NRef nref -> self#_loadNReference nref);
self#setEntry entry
end)
(* self#_showMath *)
method private egg () =
- win#mathOrListNotebook#goto_page 2;
+ self#_showEgg;
Lazy.force load_easter_egg
method private redraw_gviz ?center_on () =
self#_showSearch
method private grammar () =
- self#_loadText (Print_grammar.ebnf_of_term ());
+ self#_loadText (Print_grammar.ebnf_of_term self#script#grafite_status);
method private home () =
self#_showMath;
lastDir <- dir;
self#_loadList l
- method private _loadHBugsTutors =
- self#_showHBugs
-
method private setEntry entry =
win#browserUri#set_text (MatitaTypes.string_of_entry entry);
current_entry <- entry
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 =