X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=70079c4726a0729527cebbfb2974d774edb2c81d;hb=3969d815396a22dca5e71c5f85fa3ec66d79849e;hp=329e27e4f8c909251dac4187cd4a87be1ddc64bc;hpb=d79c894cab905cd98487192b0e5f1049875b7caa;p=helm.git

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 329e27e4f..70079c472 100644
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -1133,19 +1133,23 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       self#_showGviz
 
     method private tex () =
-      let text = String.concat "\n"
-        (List.map (fun (k,vs) -> 
-           let vs = 
-             List.sort (fun a b -> String.length a - String.length b) vs
-           in
-           let vs = 
-             if List.length vs < 4 then vs else 
-             let vs, _ = HExtlib.split_nth 4 vs in vs
-           in
-           k ^ "\t" ^ String.concat ", " vs)
-        (Utf8Macro.pp_table ())) 
-      in
-      self#_loadText text
+      let b = Buffer.create 1000 in
+      List.iter 
+        (fun tag, items -> 
+           Printf.bprintf b "%s:\n" tag;
+           List.iter 
+             (fun names, symbol ->
+                Printf.bprintf b "\t%s\t%s\n" 
+                  (Glib.Utf8.from_unichar symbol)
+                  (String.concat ", " names))
+             (List.sort 
+               (fun (_,a) (_,b) -> compare a b)
+               items);
+           Printf.bprintf b "\n")
+        (List.sort 
+          (fun (a,_) (b,_) -> compare a b)
+          (Virtuals.get_all_virtuals ()));
+      self#_loadText (Buffer.contents b)
 
     method private _loadText text =
       searchText#source_buffer#set_text text;