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

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index e1c55feb2..07143db99 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';