From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 5 Jan 2009 15:25:04 +0000 (+0000)
Subject: added some memory to virtuals eq classes
X-Git-Tag: make_still_working~4293
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4ef108b156ee542451abf57feb5bd9b501d8e977;p=helm.git

added some memory to virtuals eq classes
---

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 7965b20e4..8117947d1 100644
--- 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