helm/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 open Printf
  27
  28 (** Functions "imported" from Http_getter_misc *)
  29
  30 let normalize_dir = Http_getter_misc.normalize_dir
  31 let strip_suffix = Http_getter_misc.strip_suffix
  32
  33 let absolute_path file =
  34   if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file
  35
  36 let is_proof_script fname = true  (** TODO Zack *)
  37 let is_proof_object fname = true  (** TODO Zack *)
  38
  39 let append_phrase_sep s =
  40   if not (Pcre.pmatch ~pat:(sprintf "%s$" BuildTimeConf.phrase_sep) s) then
  41     s ^ BuildTimeConf.phrase_sep
  42   else
  43     s
  44
  45 exception History_failure
  46
  47 type 'a memento = 'a array * int * int * int  (* data, hd, tl, cur *)
  48
  49 class type ['a] history =
  50   object
  51     method add : 'a -> unit
  52     method next : 'a
  53     method previous : 'a
  54     method load: 'a memento -> unit
  55     method save: 'a memento
  56     method is_begin: bool
  57     method is_end: bool
  58   end
  59
  60 class basic_history (head, tail, cur) =
  61   object
  62     val mutable hd = head  (* insertion point *)
  63     val mutable tl = tail (* oldest inserted item *)
  64     val mutable cur = cur  (* current item for the history *)
  65
  66     method is_begin = cur <= tl
  67     method is_end = cur >= hd
  68   end
  69
  70
  71 class shell_history size =
  72   let size = size + 1 in
  73   let decr x = let x' = x - 1 in if x' < 0 then size + x' else x' in
  74   let incr x = (x + 1) mod size in
  75   object (self)
  76     val data = Array.create size ""
  77
  78     inherit basic_history (0, -1 , -1)
  79
  80     method add s =
  81       data.(hd) <- s;
  82       if tl = -1 then tl <- hd;
  83       hd <- incr hd;
  84       if hd = tl then tl <- incr tl;
  85       cur <- hd
  86     method previous =
  87       if cur = tl then raise History_failure;
  88       cur <- decr cur;
  89       data.(cur)
  90     method next =
  91       if cur = hd then raise History_failure;
  92       cur <- incr cur;
  93       if cur = hd then "" else data.(cur)
  94     method load (data', hd', tl', cur') =
  95       assert (Array.length data = Array.length data');
  96       hd <- hd'; tl <- tl'; cur <- cur';
  97       Array.blit data' 0 data 0 (Array.length data')
  98     method save = (Array.copy data, hd, tl, cur)
  99   end
 100
 101 class ['a] browser_history ?memento size init =
 102   object (self)
 103     initializer match memento with Some m -> self#load m | _ -> ()
 104     val data = Array.create size init
 105
 106     inherit basic_history (0, 0, 0)
 107
 108     method previous =
 109       if cur = tl then raise History_failure;
 110       cur <- cur - 1;
 111       if cur = ~-1 then cur <- size - 1;
 112       data.(cur)
 113     method next =
 114       if cur = hd then raise History_failure;
 115       cur <- cur + 1;
 116       if cur = size then cur <- 0;
 117       data.(cur)
 118     method add (e:'a) =
 119       if e <> data.(cur) then
 120         begin
 121           cur <- cur + 1;
 122           if cur = size then cur <- 0;
 123           if cur = tl then tl <- tl + 1;
 124           if tl = size then tl <- 0;
 125           hd <- cur;
 126           data.(cur) <- e
 127         end
 128     method load (data', hd', tl', cur') =
 129       assert (Array.length data = Array.length data');
 130       hd <- hd'; tl <- tl'; cur <- cur';
 131       Array.blit data' 0 data 0 (Array.length data')
 132     method save = (Array.copy data, hd, tl, cur)
 133   end
 134
 135 let singleton f =
 136   let instance = lazy (f ()) in
 137   fun () -> Lazy.force instance
 138
 139 let image_path n = sprintf "%s/%s" BuildTimeConf.images_dir n
 140
 141 let end_ma_RE = Pcre.regexp "\\.ma$"
 142
 143 let list_tl_at ?(equality=(==)) e l =
 144   let rec aux =
 145     function
 146     | [] -> raise Not_found
 147     | hd :: tl as l when equality hd e -> l
 148     | hd :: tl -> aux tl
 149   in
 150   aux l