added some memory to virtuals eq classes

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 7965b20e4549e9d23c263339ac81ff178953370a..8117947d11b5662c933ce4f833d059115bb6c3a6 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -395,11 +395,13 @@ class gui () =
     val mutable _only_directory = false
     val mutable font_size = default_font_size
     val mutable similarsymbols = []
+    val mutable similarsymbols_orig = []
     val clipboard = GData.clipboard Gdk.Atom.clipboard
     val primary = GData.clipboard Gdk.Atom.primary
       
     method private reset_similarsymbols =
       similarsymbols <- []; 
+      similarsymbols_orig <- []; 
       try source_buffer#delete_mark similarsymbols_tag
       with GText.No_such_mark _ -> ()
    
@@ -1124,6 +1126,8 @@ class gui () =
        true
       with Virtuals.Not_a_virtual -> false
          
+    val similar_memory = Hashtbl.create 97
+
     method private nextSimilarSymbol () = 
       let write_similarsymbol s =
         let s = Glib.Utf8.from_unichar s in
@@ -1151,17 +1155,24 @@ class gui () =
           in
           (match Virtuals.similar_symbols last_symbol with
           | [] ->  ()
-          | hd :: next ::tl ->
+          | eqclass ->
+              similarsymbols_orig <- eqclass;
+              let hd, next, tl = 
+                match 
+                  try Hashtbl.find similar_memory similarsymbols_orig  
+                  with Not_found -> Hashtbl.add similar_memory eqclass eqclass; eqclass
+                with a::b::c -> a,b,c | _ -> assert false
+              in
               let hd, tl = 
                 if hd = last_symbol then next, tl @ [hd] else hd, (next::tl)
               in
               write_similarsymbol hd;
-              similarsymbols <- tl @ [ hd ]
-          | _ -> assert false)) (* singleton eq classes are a non sense *)
+              similarsymbols <- tl @ [ hd ]))
       else 
         match similarsymbols with
         | [] -> ()
         | hd :: tl ->
+            Hashtbl.replace similar_memory similarsymbols_orig similarsymbols;
             similarsymbols <- tl @ [ hd ];
             write_similarsymbol hd