X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaMisc.ml;h=e612b88031396548b92cbc5f1ae69579d7da14b9;hb=a823c605d3a541c8d7df2bcc3c21bf459c9d25c4;hp=687cb94f052de7c1068d90ec4a88ce62c91f7a1e;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/matita/matitaMisc.ml b/matita/matita/matitaMisc.ml
index 687cb94f0..e612b8803 100644
--- a/matita/matita/matitaMisc.ml
+++ b/matita/matita/matitaMisc.ml
@@ -78,7 +78,7 @@ class shell_history size =
   let decr x = let x' = x - 1 in if x' < 0 then size + x' else x' in
   let incr x = (x + 1) mod size in
   object (self)
-    val data = Array.create size ""
+    val data = Array.make size ""
 
     inherit basic_history (0, -1 , -1)
     
@@ -106,7 +106,7 @@ class shell_history size =
 class ['a] browser_history ?memento size init =
   object (self)
     initializer match memento with Some m -> self#load m | _ -> ()
-    val data = Array.create size init
+    val data = Array.make size init
 
     inherit basic_history (0, 0, 0)
     
@@ -184,3 +184,37 @@ let out_preamble och =
    in 
    print lines;
    out_line_comment och "This file was automatically generated: do not edit"
+
+  (* is there any lablgtk2 constant corresponding to the various mouse
+   * buttons??? *)
+let left_button = 1
+let middle_button = 2
+let right_button = 3
+
+(* Font size management *)
+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 (default_font_size ())
+let font_size_observers = ref [];;
+let observe_font_size (f: int -> unit) =
+ f !current_font_size;
+ font_size_observers := f :: !font_size_observers;;
+let observe () =
+ List.iter (fun f -> f !current_font_size) !font_size_observers;;
+let get_current_font_size () = !current_font_size
+let increase_font_size () =
+ incr current_font_size; observe ()
+let decrease_font_size () =
+ decr current_font_size; observe ()
+let reset_font_size () =
+ current_font_size := default_font_size (); observe ()
+
+let gui_instance = ref None
+let set_gui (gui : MatitaGuiTypes.gui) = gui_instance := Some gui
+
+(** CSC: these functions should completely disappear (bad design) *)
+let get_gui () =
+  match !gui_instance with
+  | None -> assert false
+  | Some gui -> gui