From fc15ad45208cc2e649fa435e547ecc757fe28481 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 19 Dec 2008 21:45:45 +0000
Subject: [PATCH] better pp of virtuals

---
 helm/software/matita/matita.glade      |  4 ++--
 helm/software/matita/matitaMathView.ml | 16 ++++++++++++++--
 helm/software/matita/virtuals.ml       |  9 +++++++++
 helm/software/matita/virtuals.mli      |  2 ++
 4 files changed, 27 insertions(+), 4 deletions(-)

diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade
index 11a7321d6..fb585f50d 100644
--- a/helm/software/matita/matita.glade
+++ b/helm/software/matita/matita.glade
@@ -1307,8 +1307,8 @@
                             <child>
                               <widget class="GtkImageMenuItem" id="showUnicodeTable">
                                 <property name="visible">True</property>
-                                <property name="tooltip" translatable="yes">Show the conversion table from TeX to UTF8</property>
-                                <property name="label" translatable="yes">Tex/UTF8 table</property>
+                                <property name="tooltip" translatable="yes">Show the conversion table from TeX like sequences to UTF-8</property>
+                                <property name="label" translatable="yes">TeX/UTF-8 table</property>
                                 <property name="use_underline">True</property>
                                 <child internal-child="image">
                                   <widget class="GtkImage" id="menu-item-image20">
diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 70079c472..7cb2aa7cb 100644
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -1134,12 +1134,24 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
     method private tex () =
       let b = Buffer.create 1000 in
+      Printf.bprintf b "UTF-8 equivalence classes (rotate with ALT-L):\n\n";
+      List.iter 
+        (fun l ->
+           List.iter (fun sym ->
+             Printf.bprintf b "  %s" (Glib.Utf8.from_unichar sym) 
+           ) l;
+           Printf.bprintf b "\n";
+        )
+        (List.sort 
+          (fun l1 l2 -> compare (List.hd l1) (List.hd l2))
+          (Virtuals.get_all_eqclass ()));
+      Printf.bprintf b "\n\nVirtual keys (trigger with ALT-L):\n\n";
       List.iter 
         (fun tag, items -> 
-           Printf.bprintf b "%s:\n" tag;
+           Printf.bprintf b "  %s:\n" tag;
            List.iter 
              (fun names, symbol ->
-                Printf.bprintf b "\t%s\t%s\n" 
+                Printf.bprintf b "  \t%s\t%s\n" 
                   (Glib.Utf8.from_unichar symbol)
                   (String.concat ", " names))
              (List.sort 
diff --git a/helm/software/matita/virtuals.ml b/helm/software/matita/virtuals.ml
index 4d7b91507..229e780c2 100644
--- a/helm/software/matita/virtuals.ml
+++ b/helm/software/matita/virtuals.ml
@@ -56,4 +56,13 @@ let similar_symbols symbol =
   with Not_found -> []
 ;;
 
+let get_all_eqclass () =
+  let rc = ref [] in
+  Hashtbl.iter 
+    (fun k v ->
+      if not (List.mem v !rc) then
+        rc := v :: !rc)
+    classes;
+  !rc
+;;
 
diff --git a/helm/software/matita/virtuals.mli b/helm/software/matita/virtuals.mli
index ec77c244b..09e350a3a 100644
--- a/helm/software/matita/virtuals.mli
+++ b/helm/software/matita/virtuals.mli
@@ -11,4 +11,6 @@ val get_all_virtuals : unit -> (tag * (string list * symbol) list) list
 val add_eqclass: symbol list -> unit
 val similar_symbols: symbol -> symbol list
 
+val get_all_eqclass: unit -> symbol list list
+
 (* (["\\lambda";"\\"], "λ", ["logics";"letters"]) *)
-- 
2.39.2