Previous patch improved: we now use an ad-hoc wrapper for Grammar.parsable

[helm.git] / matita / matita / matitaMathView.ml

diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml
index 78e0a13a52364e2addcb18570fa1bd8babfb4997..a8f20aa1863c5765565618f87b8a68ace7b892dd 100644 (file)
--- 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;
@@ -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 =