]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/matitaMisc.ml
exportation completed!!
[helm.git] / helm / software / 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 (self)
81     val data = Array.create 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.create 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 :: tl as l when equality hd e -> l
153     | hd :: tl -> aux tl
154   in
155   aux l
156
157 let shutup () = 
158   HLog.set_log_callback (fun _ _ -> ());
159   let out = open_out "/dev/null" in
160   Unix.dup2 (Unix.descr_of_out_channel out) (Unix.descr_of_out_channel stderr)
161