X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaMathView.ml;h=a8f20aa1863c5765565618f87b8a68ace7b892dd;hb=4e251fb6d7fab1c489c5141759bb896f116b1b91;hp=f418abe6f8e658dc3b78eadc9610b9ed380a865a;hpb=f6b7c6ae353e014761a3d24dbc87e00d828d7f2d;p=helm.git diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index f418abe6f..a8f20aa18 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -620,7 +620,7 @@ object (self) val mutable current_mathml = None method nload_sequent: - 'status. #NCicCoercion.status as 'status -> NCic.metasenv -> + 'status. #ApplyTransformation.status as 'status -> NCic.metasenv -> NCic.substitution -> int -> unit = fun status metasenv subst metano -> let sequent = List.assoc metano metasenv in @@ -637,7 +637,7 @@ object (self) self#load_root ~root:txt method load_nobject : - 'status. #NCicCoercion.status as 'status -> NCic.obj -> unit + 'status. #ApplyTransformation.status as 'status -> NCic.obj -> unit = fun status obj -> let txt = ApplyTransformation.ntxt_of_cic_object ~map_unicode_to_tex:false 80 status obj in @@ -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 -> + 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; @@ -808,7 +808,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = self#render_page status ~page ~goal_switch)) method private render_page: - 'status. #NCicCoercion.status as 'status -> page:int -> + 'status. #ApplyTransformation.status as 'status -> page:int -> goal_switch:Stack.switch -> unit = fun status ~page ~goal_switch -> (match goal_switch with @@ -825,7 +825,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = List.assoc goal_switch goal2win () with Not_found -> assert false) - method goto_sequent: 'status. #NCicCoercion.status as 'status -> int -> unit + method goto_sequent: 'status. #ApplyTransformation.status as 'status -> int -> unit = fun status goal -> let goal_switch, page = try @@ -1036,12 +1036,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 ()); @@ -1058,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" *) @@ -1099,12 +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 _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 @@ -1136,7 +1127,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | `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) @@ -1150,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 () = @@ -1226,7 +1216,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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; @@ -1254,9 +1244,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 @@ -1280,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 =