]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/matitaMisc.ml
web site update
[helm.git] / matita / matita / matitaMisc.ml
1 (* Copyright (C) 2004-2005, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 (* $Id$ *)
27
28 open Printf
29
30 (** Functions "imported" from Http_getter_misc *)
31
32 let normalize_dir = Http_getter_misc.normalize_dir
33 let strip_suffix ~suffix s = 
34   try 
35     Http_getter_misc.strip_suffix ~suffix s
36   with Invalid_argument _ -> s
37
38 let absolute_path file =
39   if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file
40   
41 let is_proof_script _fname = true  (** TODO Zack *)
42 let is_proof_object _fname = true  (** TODO Zack *)
43
44 let append_phrase_sep s =
45   if not (Pcre.pmatch ~pat:(sprintf "%s$" BuildTimeConf.phrase_sep) s) then
46     s ^ BuildTimeConf.phrase_sep
47   else
48     s
49
50 exception History_failure
51
52 type 'a memento = 'a array * int * int * int  (* data, hd, tl, cur *)
53
54 class type ['a] history =
55   object
56     method add : 'a -> unit
57     method next : 'a
58     method previous : 'a
59     method load: 'a memento -> unit
60     method save: 'a memento
61     method is_begin: bool
62     method is_end: bool
63   end
64
65 class basic_history (head, tail, cur) =
66   object
67     val mutable hd = head  (* insertion point *)
68     val mutable tl = tail (* oldest inserted item *)
69     val mutable cur = cur  (* current item for the history *)
70     
71     method is_begin = cur <= tl
72     method is_end = cur >= hd
73   end
74   
75   
76 class shell_history size =
77   let size = size + 1 in
78   let decr x = let x' = x - 1 in if x' < 0 then size + x' else x' in
79   let incr x = (x + 1) mod size in
80   object
81     val data = Array.make size ""
82
83     inherit basic_history (0, -1 , -1)
84     
85     method add s =
86       data.(hd) <- s;
87       if tl = -1 then tl <- hd;
88       hd <- incr hd;
89       if hd = tl then tl <- incr tl;
90       cur <- hd
91     method previous =
92       if cur = tl then raise History_failure;
93       cur <- decr cur;
94       data.(cur)
95     method next =
96       if cur = hd then raise History_failure;
97       cur <- incr cur;
98       if cur = hd then "" else data.(cur)
99     method load (data', hd', tl', cur') =
100       assert (Array.length data = Array.length data');
101       hd <- hd'; tl <- tl'; cur <- cur';
102       Array.blit data' 0 data 0 (Array.length data')
103     method save = (Array.copy data, hd, tl, cur)
104   end
105
106 class ['a] browser_history ?memento size init =
107   object (self)
108     initializer match memento with Some m -> self#load m | _ -> ()
109     val data = Array.make size init
110
111     inherit basic_history (0, 0, 0)
112     
113     method previous =
114       if cur = tl then raise History_failure;
115       cur <- cur - 1;
116       if cur = ~-1 then cur <- size - 1;
117       data.(cur)
118     method next =
119       if cur = hd then raise History_failure;
120       cur <- cur + 1;
121       if cur = size then cur <- 0;
122       data.(cur)
123     method add (e:'a) =
124       if e <> data.(cur) then
125         begin
126           cur <- cur + 1;
127           if cur = size then cur <- 0;
128           if cur = tl then tl <- tl + 1;
129           if tl = size then tl <- 0;
130           hd <- cur;
131           data.(cur) <- e
132         end
133     method load (data', hd', tl', cur') =
134       assert (Array.length data = Array.length data');
135       hd <- hd'; tl <- tl'; cur <- cur';
136       Array.blit data' 0 data 0 (Array.length data')
137     method save = (Array.copy data, hd, tl, cur)
138   end
139
140 let singleton f =
141   let instance = lazy (f ()) in
142   fun () -> Lazy.force instance
143
144 let image_path n = sprintf "%s/%s" BuildTimeConf.images_dir n
145
146 let end_ma_RE = Pcre.regexp "\\.ma$"
147
148 let list_tl_at ?(equality=(==)) e l =
149   let rec aux =
150     function
151     | [] -> raise Not_found
152     | hd :: _ as l when equality hd e -> l
153     | _ :: tl -> aux tl
154   in
155   aux l
156
157 let shutup () = 
158   HLog.set_log_callback (fun _ _ -> ())
159 (*
160   let out = open_out "/dev/null" in
161   Unix.dup2 (Unix.descr_of_out_channel out) (Unix.descr_of_out_channel stderr)
162 *)
163               
164 (* FG: out_preamble *********************************************************)
165
166 let out_comment och s =
167    let s = if s <> "" && s.[0] = '*' then "#" ^ s else s in
168    Printf.fprintf och "%s%s%s\n\n" "(*" s "*)" 
169  
170 let out_line_comment och s =
171    let l = 70 - String.length s in
172    let s = Printf.sprintf " %s %s" s (String.make l '*') in
173    out_comment och s
174
175 let out_preamble och =
176    let rt_base_dir = Filename.dirname Sys.argv.(0) in
177    let path = Filename.concat rt_base_dir "matita.ma.templ" in
178    let lines = 14 in
179    let ich = open_in path in
180    let rec print i =
181       if i > 0 then 
182          let s = input_line ich in
183          begin Printf.fprintf och "%s\n" s; print (pred i) end
184    in 
185    print lines;
186    out_line_comment och "This file was automatically generated: do not edit"
187
188   (* is there any lablgtk2 constant corresponding to the various mouse
189    * buttons??? *)
190 let left_button = 1
191 let middle_button = 2
192 let right_button = 3
193
194 (* Font size management *)
195 let default_font_size () =
196   Helm_registry.get_opt_default Helm_registry.int
197     ~default:BuildTimeConf.default_font_size "matita.font_size"
198 let current_font_size = ref (default_font_size ())
199 let font_size_observers = ref [];;
200 let observe_font_size (f: int -> unit) =
201  f !current_font_size;
202  font_size_observers := f :: !font_size_observers;;
203 let observe () =
204  List.iter (fun f -> f !current_font_size) !font_size_observers;;
205 let get_current_font_size () = !current_font_size
206 let increase_font_size () =
207  incr current_font_size; observe ()
208 let decrease_font_size () =
209  decr current_font_size; observe ()
210 let reset_font_size () =
211  current_font_size := default_font_size (); observe ()
212
213 let gui_instance = ref None
214 let set_gui (gui : MatitaGuiTypes.gui) = gui_instance := Some gui
215
216 (** CSC: these functions should completely disappear (bad design) *)
217 let get_gui () =
218   match !gui_instance with
219   | None -> assert false
220   | Some gui -> gui