X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=ff79f54ed05ee8d59a7bcfde9a1bff29538eef76;hb=10f29fdd78ee089a9a94446207b543d33d6c851c;hp=b8dd3f1bdcb5bb2d5e0f01428aaf08306ac06fec;hpb=1c361432e4fd08de7a85c108ccfc6990d6ffd141;p=helm.git diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index b8dd3f1bd..ff79f54ed 100644 --- 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