Use of standard OCaml syntax

[helm.git] / matita / matita / matitaMisc.ml

diff --git a/matita/matita/matitaMisc.ml b/matita/matita/matitaMisc.ml
index 6e733cd1f893f56954b6dd429d1eaf0c6a15504c..df124751f1fe6e21480fb45a133ecaa0e2c8a79f 100644 (file)
--- a/matita/matita/matitaMisc.ml
+++ b/matita/matita/matitaMisc.ml
@@ -38,8 +38,8 @@ let strip_suffix ~suffix s =
 let absolute_path file =
   if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file
   
-let is_proof_script fname = true  (** TODO Zack *)
-let is_proof_object fname = true  (** TODO Zack *)
+let is_proof_script _fname = true  (* TODO Zack *)
+let is_proof_object _fname = true  (* TODO Zack *)
 
 let append_phrase_sep s =
   if not (Pcre.pmatch ~pat:(sprintf "%s$" BuildTimeConf.phrase_sep) s) then
@@ -77,8 +77,8 @@ class shell_history size =
   let size = size + 1 in
   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 ""
+  object
+    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)
     
@@ -149,18 +149,11 @@ let list_tl_at ?(equality=(==)) e l =
   let rec aux =
     function
     | [] -> raise Not_found
-    | hd :: tl as l when equality hd e -> l
-    | hd :: tl -> aux tl
+    | hd :: _ as l when equality hd e -> l
+    | _ :: tl -> aux tl
   in
   aux l
 
-let shutup () = 
-  HLog.set_log_callback (fun _ _ -> ())
-(*
-  let out = open_out "/dev/null" in
-  Unix.dup2 (Unix.descr_of_out_channel out) (Unix.descr_of_out_channel stderr)
-*)
-              
 (* FG: out_preamble *********************************************************)
 
 let out_comment och s =
@@ -191,14 +184,24 @@ 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 ~-1
+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
-let decrease_font_size () = decr current_font_size
-let reset_font_size () = current_font_size := default_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