X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=7f1917cfe1cf5ce6c3642966aaebd54ad1846546;hb=2bd1dbc6fdad64f989089165a4e7367c072d2656;hp=fc1b7d47022935c7a83994218fc5fec6052ba787;hpb=86e607e77de78302e52b6d1cb1381f5a377be456;p=helm.git

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index fc1b7d470..7f1917cfe 100644
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -288,14 +288,13 @@ object (self)
     reductions_menu_item#set_submenu reductions;
     tactics_menu_item#set_submenu tactics;
     let normalize = add_menu_item ~menu:reductions ~label:"Normalize" () in
-    let reduce = add_menu_item ~menu:reductions ~label:"Reduce" () in
     let simplify = add_menu_item ~menu:reductions ~label:"Simplify" () in
     let whd = add_menu_item ~menu:reductions ~label:"Weak head" () in
     menu#append (GMenu.separator_item ());
     let copy = add_menu_item ~stock:`COPY () in
     let gui = get_gui () in
     List.iter (fun item -> item#misc#set_sensitive gui#canCopy)
-      [ copy; check; normalize; reduce; simplify; whd ];
+      [ copy; check; normalize; simplify; whd ];
     let reduction_action kind () =
       let pat = self#tactic_text_pattern_of_selection in
       let statement =
@@ -311,7 +310,6 @@ object (self)
       (MatitaScript.current ())#advance ~statement () in
     connect_menu_item copy gui#copy;
     connect_menu_item normalize (reduction_action `Normalize);
-    connect_menu_item reduce (reduction_action `Reduce);
     connect_menu_item simplify (reduction_action `Simpl);
     connect_menu_item whd (reduction_action `Whd);
     menu#popup ~button:right_button ~time
@@ -620,11 +618,11 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
 
     method load_logo =
      notebook#set_show_tabs false;
-     notebook#append_page logo
+     ignore(notebook#append_page logo)
 
     method load_logo_with_qed =
      notebook#set_show_tabs false;
-     notebook#append_page logo_with_qed
+     ignore(notebook#append_page logo_with_qed)
 
     method reset =
       cicMathView#remove_selections;
@@ -698,7 +696,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       let add_tab markup goal_switch =
         let goal = Stack.goal_of_switch goal_switch in
         if not (List.mem goal !added_goals) then begin
-          notebook#append_page ~tab_label:(tab_label markup) (win goal_switch);
+          ignore(notebook#append_page 
+            ~tab_label:(tab_label markup) (win goal_switch));
           page2goal <- (!page, goal_switch) :: page2goal;
           goal2page <- (goal_switch, !page) :: goal2page;
           incr page;
@@ -903,10 +902,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       ignore (win#toplevel#event#connect#delete (fun _ ->
         let my_id = Oo.id self in
         cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers;
-        if !cicBrowsers = [] &&
-          Helm_registry.get "matita.mode" = "cicbrowser"
-        then
-          GMain.quit ();
         false));
       ignore(win#whelpResultTreeview#connect#row_activated 
         ~callback:(fun _ _ ->
@@ -931,8 +926,12 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
         match self#currentCicUri with
         | Some uri -> self#load (`Metadata (`Deps (`Back, uri)))
         | None -> ());
+      (* remove hbugs *)
+      (*
       connect_menu_item win#hBugsTutorsMenuItem (fun () ->
         self#load (`HBugs `Tutors));
+      *)
+      win#hBugsTutorsMenuItem#misc#hide ();
       connect_menu_item win#browserUrlMenuItem (fun () ->
         win#browserUri#entry#misc#grab_focus ());
 
@@ -1040,7 +1039,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           | `About `Coercions -> self#coerchgraph true ()
           | `Check term -> self#_loadCheck term
           | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
-          | `Development d -> self#_showDevelDeps d
           | `Dir dir -> self#_loadDir dir
           | `HBugs `Tutors -> self#_loadHBugsTutors
           | `Metadata (`Deps ((`Fwd | `Back) as dir, uri)) ->
@@ -1131,16 +1129,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       win#browserUri#entry#set_text (MatitaTypes.string_of_entry entry);
       current_entry <- entry
 
-    method private _showDevelDeps d =
-      match MatitamakeLib.development_for_name d with
-      | None -> ()
-      | Some devel ->
-          (match MatitamakeLib.dot_for_development devel with
-          | None -> ()
-          | Some fname ->
-              gviz#load_graph_from_file ~gviz_cmd:"tred | dot" fname;
-              self#_showGviz)
-
     method private _loadObj obj =
       (* showMath must be done _before_ loading the document, since if the
        * widget is not mapped (hidden by the notebook) the document is not