Bertrand's conjecture (weak), some work in progress

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

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index b8dd3f1bdcb5bb2d5e0f01428aaf08306ac06fec..ff79f54ed05ee8d59a7bcfde9a1bff29538eef76 100644 (file)
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -620,11 +620,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 +698,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 +904,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 _ _ ->
@@ -1044,7 +1041,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)) ->
@@ -1135,16 +1131,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