1 (* Copyright (C) 2004-2005, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
30 (** Functions "imported" from Http_getter_misc *)
32 let normalize_dir = Http_getter_misc.normalize_dir
33 let strip_suffix ~suffix s =
35 Http_getter_misc.strip_suffix ~suffix s
36 with Invalid_argument _ -> s
38 let absolute_path file =
39 if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file
41 let is_proof_script _fname = true (** TODO Zack *)
42 let is_proof_object _fname = true (** TODO Zack *)
44 let append_phrase_sep s =
45 if not (Pcre.pmatch ~pat:(sprintf "%s$" BuildTimeConf.phrase_sep) s) then
46 s ^ BuildTimeConf.phrase_sep
50 exception History_failure
52 type 'a memento = 'a array * int * int * int (* data, hd, tl, cur *)
54 class type ['a] history =
56 method add : 'a -> unit
59 method load: 'a memento -> unit
60 method save: 'a memento
65 class basic_history (head, tail, cur) =
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 *)
71 method is_begin = cur <= tl
72 method is_end = cur >= hd
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
81 val data = Array.make size ""
83 inherit basic_history (0, -1 , -1)
87 if tl = -1 then tl <- hd;
89 if hd = tl then tl <- incr tl;
92 if cur = tl then raise History_failure;
96 if cur = hd then raise History_failure;
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)
106 class ['a] browser_history ?memento size init =
108 initializer match memento with Some m -> self#load m | _ -> ()
109 val data = Array.make size init
111 inherit basic_history (0, 0, 0)
114 if cur = tl then raise History_failure;
116 if cur = ~-1 then cur <- size - 1;
119 if cur = hd then raise History_failure;
121 if cur = size then cur <- 0;
124 if e <> data.(cur) then
127 if cur = size then cur <- 0;
128 if cur = tl then tl <- tl + 1;
129 if tl = size then tl <- 0;
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)
141 let instance = lazy (f ()) in
142 fun () -> Lazy.force instance
144 let image_path n = sprintf "%s/%s" BuildTimeConf.images_dir n
146 let end_ma_RE = Pcre.regexp "\\.ma$"
148 let list_tl_at ?(equality=(==)) e l =
151 | [] -> raise Not_found
152 | hd :: _ as l when equality hd e -> l
158 HLog.set_log_callback (fun _ _ -> ())
160 let out = open_out "/dev/null" in
161 Unix.dup2 (Unix.descr_of_out_channel out) (Unix.descr_of_out_channel stderr)
164 (* FG: out_preamble *********************************************************)
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 "*)"
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
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
179 let ich = open_in path in
182 let s = input_line ich in
183 begin Printf.fprintf och "%s\n" s; print (pred i) end
186 out_line_comment och "This file was automatically generated: do not edit"
188 (* is there any lablgtk2 constant corresponding to the various mouse
191 let middle_button = 2
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;;
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 ()
213 let gui_instance = ref None
214 let set_gui (gui : MatitaGuiTypes.gui) = gui_instance := Some gui
216 (** CSC: these functions should completely disappear (bad design) *)
218 match !gui_instance with
219 | None -> assert false