X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaMathView.ml;h=280ade3ee11ac559fa3494d0fe2e4d81175a8bb8;hb=16250ed29f9200595694cd49dfc1aed76280dcb9;hp=f418abe6f8e658dc3b78eadc9610b9ed380a865a;hpb=f6b7c6ae353e014761a3d24dbc87e00d828d7f2d;p=helm.git

diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml
index f418abe6f..280ade3ee 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. #LexiconTypes.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. #LexiconTypes.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
@@ -728,7 +728,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       self#script#setGoal None
 
     method nload_sequents : 'status. #NTacStatus.tac_status as 'status -> unit
-    = fun status ->
+    = fun (status : #NTacStatus.tac_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. #LexiconTypes.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. #LexiconTypes.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 ());
 
@@ -1104,7 +1098,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     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 back () =
       try
@@ -1136,7 +1129,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)
@@ -1226,7 +1218,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 +1246,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