From dfad83fbd13bfec107d1f7a9533c90b7bb862dcf Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 18 Jun 2005 11:52:13 +0000 Subject: [PATCH] fixed increase/decrease size feature --- helm/matita/matita.ml | 1 + helm/matita/matitaMathView.ml | 1 - 2 files changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 34b41e4cc..40592d001 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -65,6 +65,7 @@ let _ = gui#resetFontSize (); MatitaMathView.reset_font_size (); MatitaMathView.update_font_sizes ())); + MatitaMathView.reset_font_size (); (* disambiguator callback *) MatitaDisambiguator.set_choose_uris_callback (MatitaGui.interactive_uri_choice ()); diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 776a9ada5..5b1f4d5b3 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -76,7 +76,6 @@ class clickableMathView obj = method set_href_callback f = href_callback <- f initializer - current_font_size := default_font_size (); self#set_font_size !current_font_size; ignore (self#connect#selection_changed self#choose_selection); ignore (self#connect#click (fun (gdome_elt, _, _, _) -> -- 2.39.2