X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMisc.ml;h=a35a57ed644943103e5c5a9e22806abc28445df9;hb=349a0e23813a7f33853e1f8fe48230276ac22934;hp=e1c55feb204e02ca0e3c9354d9b1aa7eaa48c2b2;hpb=de4483296d06aac3df4da10d5401b1f97c4350ab;p=helm.git

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index e1c55feb2..a35a57ed6 100644
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -139,12 +139,15 @@ class ['a] browser_history ?memento size init =
       if cur = size then cur <- 0;
       data.(cur)
     method add (e:'a) =
-      cur <- cur + 1;
-      if cur = size then cur <- 0;
-      if cur = tl then tl <- tl + 1;
-      if tl = size then tl <- 0;
-      hd <- cur;
-      data.(cur) <- e
+      if e <> data.(cur) then
+        begin
+          cur <- cur + 1;
+          if cur = size then cur <- 0;
+          if cur = tl then tl <- tl + 1;
+          if tl = size then tl <- 0;
+          hd <- cur;
+          data.(cur) <- e
+        end
     method load (data', hd', tl', cur') =
       assert (Array.length data = Array.length data');
       hd <- hd'; tl <- tl'; cur <- cur';
@@ -189,3 +192,5 @@ let qualify status name = get_string_option status "baseuri" ^ "/" ^ name
 
 let unopt = function None -> failwith "unopt: None" | Some v -> v
 
+let image_path n = sprintf "%s/%s" BuildTimeConf.images_dir n
+