X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=7f1917cfe1cf5ce6c3642966aaebd54ad1846546;hb=186c1171d37f5d1cde9bb6f38a863be16debf3f0;hp=23f57820df80601337c8ba86ff5b958a0f428383;hpb=cd9eaee0b18ee5988a3b846a5e30e3e64cb9a2fe;p=helm.git

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 23f57820d..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
@@ -904,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 _ _ ->
@@ -1045,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)) ->
@@ -1136,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