From: Enrico Tassi Date: Thu, 16 Jun 2005 11:55:21 +0000 (+0000) Subject: added decrease and increase font size fantafeature X-Git-Tag: INDEXING_NO_PROOFS~135 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=522bfe4fd22804ff7fb0013697721504003a6606;p=helm.git added decrease and increase font size fantafeature --- diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in index 6b35fda1f..b5581fb8e 100644 --- a/helm/matita/buildTimeConf.ml.in +++ b/helm/matita/buildTimeConf.ml.in @@ -33,7 +33,8 @@ let base_uri = "cic:/matita";; let phrase_sep = ".";; let blank_uri = "about:blank";; let current_proof_uri = "about:current_proof";; -let default_script_font = "Monospace 10";; +let default_font_size = 10;; +let script_font = "Monospace";; let runtime_base_dir = "@RT_BASE_DIR@";; let images_dir = runtime_base_dir ^ "/icons" diff --git a/helm/matita/matita.conf.xml.sample b/helm/matita/matita.conf.xml.sample index d28c809d0..a425dba55 100644 --- a/helm/matita/matita.conf.xml.sample +++ b/helm/matita/matita.conf.xml.sample @@ -6,7 +6,7 @@ cic:/matita/ .matita/xml mario - + false
diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 5bb01b0f5..47d8a3d1e 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -881,7 +881,7 @@ Copyright (C) 2005, True - + True gtk-new 1 @@ -902,7 +902,7 @@ Copyright (C) 2005, - + True gtk-open 1 @@ -923,7 +923,7 @@ Copyright (C) 2005, - + True gtk-save 1 @@ -943,7 +943,7 @@ Copyright (C) 2005, True - + True gtk-save-as 1 @@ -970,7 +970,7 @@ Copyright (C) 2005, - + True gtk-quit 1 @@ -1005,22 +1005,22 @@ Copyright (C) 2005, - + True - New Cic Browser + Show/Hide the tactics buttons bar + View Tactics Bar True - + True + - + True - Show/Hide the tactics buttons bar - View Tactics Bar + New Cic Browser True - True - + @@ -1033,6 +1033,41 @@ Copyright (C) 2005, + + + + True + + + + + + True + Increase Font Size + True + + + + + + + + True + Decrease Font Size + True + + + + + + + + True + Normal Font Size + True + + + diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 5433a898b..6c3459c4a 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -52,6 +52,19 @@ let gui = MatitaGui.instance () let _ = ignore (gui#main#newCicBrowserMenuItem#connect#activate (fun _ -> ignore (MatitaMathView.cicBrowser ()))); + (* font sizes *) + ignore (gui#main#increaseFontSizeMenuItem#connect#activate (fun _ -> + gui#increaseFontSize (); + MatitaMathView.increase_font_size (); + MatitaMathView.update_font_sizes ())); + ignore (gui#main#decreaseFontSizeMenuItem#connect#activate (fun _ -> + gui#decreaseFontSize (); + MatitaMathView.decrease_font_size (); + MatitaMathView.update_font_sizes ())); + ignore (gui#main#normalFontSizeMenuItem#connect#activate (fun _ -> + gui#resetFontSize (); + MatitaMathView.reset_font_size (); + MatitaMathView.update_font_sizes ())); (* disambiguator callback *) MatitaDisambiguator.set_choose_uris_callback (MatitaGui.interactive_uri_choice ()); diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 66cc8b0ff..cdbfc799a 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -77,11 +77,16 @@ class gui () = ~packing:main#scriptScrolledWin#add () in + let default_font_size = + Helm_registry.get_opt_default Helm_registry.int + ~default:BuildTimeConf.default_font_size "matita.font_size" + in let source_buffer = source_view#source_buffer in object (self) val mutable chosen_file = None val mutable _ok_not_exists = false - val mutable script_fname = None + val mutable script_fname = None + val mutable font_size = default_font_size initializer (* glade's check widgets *) @@ -267,19 +272,7 @@ class gui () = "\n"; advance ()); (* script monospace font stuff *) - let font = - Helm_registry.get_opt_default Helm_registry.string - ~default:BuildTimeConf.default_script_font "matita.script_font" - in -(* let monospace_tag = - source_buffer#create_tag [`FONT_DESC font] - in *) - self#sourceView#misc#modify_font_by_name font; -(* let _ = - source_buffer#connect#changed ~callback:(fun _ -> - let start, stop = source_buffer#bounds in - source_buffer#apply_tag monospace_tag start stop) - in *) + self#updateFontSize (); (* debug menu *) self#main#debugMenu#misc#hide (); (* status bar *) @@ -381,6 +374,22 @@ class gui () = GtkThread.main (); !text + method private updateFontSize () = + self#sourceView#misc#modify_font_by_name + (sprintf "%s %d" BuildTimeConf.script_font font_size) + + method increaseFontSize () = + font_size <- font_size + 1; + self#updateFontSize () + + method decreaseFontSize () = + font_size <- font_size - 1; + self#updateFontSize () + + method resetFontSize () = + font_size <- default_font_size; + self#updateFontSize () + end let gui () = diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index 42922140c..80c183fac 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -77,6 +77,11 @@ object method askText: ?title:string -> ?msg:string -> unit -> string option method loadScript: string -> unit + + (** {3 Fonts} *) + method increaseFontSize: unit -> unit + method decreaseFontSize: unit -> unit + method resetFontSize: unit -> unit end diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 75541ed9d..9c8ef985b 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -56,6 +56,16 @@ object (self) method private script = MatitaScript.instance () end +let cicBrowsers = ref [] + +let default_font_size () = + Helm_registry.get_opt_default Helm_registry.int + ~default:BuildTimeConf.default_font_size "matita.font_size" +let current_font_size = ref ~-1 +let increase_font_size () = incr current_font_size +let decrease_font_size () = decr current_font_size +let reset_font_size () = current_font_size := default_font_size () + class clickableMathView obj = let href = Gdome.domString "href" in let xref = Gdome.domString "xref" in @@ -66,6 +76,8 @@ 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, _, _, _) -> match gdome_elt with @@ -95,6 +107,10 @@ class clickableMathView obj = match gdome_elt with | Some elt -> aux elt | None -> self#set_selection None + + method update_font_size = + self#set_font_size !current_font_size + end let clickableMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity = @@ -111,7 +127,7 @@ class sequentViewer obj = inherit clickableMathView obj val mutable current_infos = None - + method get_selected_terms = let selections = self#get_selections in list_map_fail @@ -287,8 +303,6 @@ type term_source = exception Browser_failure of string -let cicBrowsers = ref [] - class type cicBrowser = object method load: MatitaTypes.mathViewer_entry -> unit @@ -581,6 +595,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_historyAdd entry end + (** {2 methods accessing underlying GtkMathView} *) + + method updateFontSize = mathView#set_font_size !current_font_size + (** {2 methods used by constructor only} *) method win = win @@ -620,8 +638,6 @@ let cicBrowser () = let history = new MatitaMisc.browser_history size (`About `Blank) in aux history -let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers - let default_sequentViewer () = sequentViewer ~show:true () let sequentViewer_instance = MatitaMisc.singleton default_sequentViewer @@ -646,3 +662,10 @@ let mathViewer () = method show_uri_list ?(reuse=false) ~entry l = (self#get_browser reuse)#load entry end + +let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers + +let update_font_sizes () = + List.iter (fun b -> b#updateFontSize) !cicBrowsers; + (sequentViewer_instance ())#update_font_size + diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index b11befe4e..ed57b886c 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -32,6 +32,8 @@ class type clickableMathView = (** set hyperlink callback. None disable hyperlink handling *) method set_href_callback: (string -> unit) option -> unit + + method update_font_size: unit end class type sequentViewer = @@ -93,7 +95,14 @@ val sequentsViewer: val cicBrowser: unit -> cicBrowser -val refresh_all_browsers: unit -> unit +(** mathview wide functions *) + +val increase_font_size: unit -> unit +val decrease_font_size: unit -> unit +val reset_font_size: unit -> unit + +val refresh_all_browsers: unit -> unit (** act on all cicBrowsers *) +val update_font_sizes: unit -> unit (** {2 singleton instances} *) diff --git a/helm/matita/tests/record.ma b/helm/matita/tests/record.ma index 43e8e5d44..61dec1d7e 100644 --- a/helm/matita/tests/record.ma +++ b/helm/matita/tests/record.ma @@ -1,5 +1,7 @@ record empty : Type \def {}. +inductive True : Prop \def I: True. + record pippo : Type \def { a: Set ;