0.5.3

diff --git a/helm/software/configure.ac b/helm/software/configure.ac
index ef4bb5da28384082469fdf744c0a456c58247cc4..333761076666b2e2f8354d92b386039324babaa8 100644 (file)
--- a/helm/software/configure.ac
+++ b/helm/software/configure.ac
@@ -5,7 +5,7 @@ AC_INIT(matita/matitaTypes.ml)
 DEBUG_DEFAULT="true"
 DEFAULT_DBHOST="mysql://mowgli.cs.unibo.it"
 RT_BASE_DIR_DEFAULT="`pwd`/matita"
-MATITA_VERSION="0.5.2"
+MATITA_VERSION="0.5.3"
 DISTRIBUTED="no"  # "yes" for distributed tarballs
 # End of distribution settings
 

diff --git a/helm/software/matita/dist/ChangeLog b/helm/software/matita/dist/ChangeLog
index 63b4e785b169e854f8e07993b4a4a310e1036b28..2ff51705c3121e12ff09f347ab625e30bb46c2b6 100644 (file)
--- a/helm/software/matita/dist/ChangeLog
+++ b/helm/software/matita/dist/ChangeLog
@@ -1,4 +1,4 @@
-0.5.3  - ?/7/2008 - bugfix release
+0.5.3  - 23/7/2008 - bugfix release
        * many fixes concerning the CProp hiearchy
        * coercion database simplified
        * coercion hiding now works properly for coercions to funclass
@@ -8,6 +8,7 @@
        * \infrule layout added, allows to display readable fractions
        * better window for terms grammar and TeX/Unicode
        * fixed a bug in the positivity check not considering some subterms
+       * fixed some GUI glitches thanks to glade-3
 
 0.5.2  - 2/7/2008 - better-usability-for-the-working-constructivist release
        * refinement of match fixed to prevent useless unfolding,

diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade
index 14bfea0dcf6be49fbc8ff9e70754dcb69a93d175..34121dd9f9d651ea5fe45465818dadd562033847 100644 (file)
--- a/helm/software/matita/matita.glade
+++ b/helm/software/matita/matita.glade
@@ -3,12 +3,12 @@
 <!--*- mode: xml -*-->
 <glade-interface>
   <widget class="GtkWindow" id="BrowserWin">
-    <property name="width_request">640</property>
+    <property name="width_request">500</property>
     <property name="height_request">480</property>
     <property name="visible">True</property>
     <property name="title" translatable="yes">Cic browser</property>
     <property name="window_position">GTK_WIN_POS_CENTER_ON_PARENT</property>
-    <property name="default_width">640</property>
+    <property name="default_width">500</property>
     <property name="default_height">480</property>
     <property name="destroy_with_parent">True</property>
     <property name="transient_for">MainWin</property>
@@ -1289,13 +1289,27 @@
                               </widget>
                             </child>
                             <child>
-                              <widget class="GtkImageMenuItem" id="showTermGrammarMenuItem">
+                              <widget class="GtkMenuItem" id="showTermGrammarMenuItem">
                                 <property name="visible">True</property>
-                                <property name="tooltip" translatable="yes">Displays the term grammar</property>
-                                <property name="label" translatable="yes">Show term's grammar</property>
+                                <property name="tooltip" translatable="yes">Displays the terms grammar as extended by the user</property>
+                                <property name="label" translatable="yes">Terms grammar</property>
                                 <property name="use_underline">True</property>
                               </widget>
                             </child>
+                            <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="use_underline">True</property>
+                                <child internal-child="image">
+                                  <widget class="GtkImage" id="menu-item-image20">
+                                    <property name="visible">True</property>
+                                    <property name="stock">gtk-select-font</property>
+                                  </widget>
+                                </child>
+                              </widget>
+                            </child>
                           </widget>
                         </child>
                       </widget>
@@ -1338,14 +1352,6 @@
                                 </child>
                               </widget>
                             </child>
-                            <child>
-                              <widget class="GtkImageMenuItem" id="showUnicodeTable">
-                                <property name="visible">True</property>
-                                <property name="tooltip" translatable="yes">Displays the Tex/Unicode table</property>
-                                <property name="label" translatable="yes">Show Tex/Unicode table</property>
-                                <property name="use_underline">True</property>
-                              </widget>
-                            </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="aboutMenuItem">
                                 <property name="visible">True</property>

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 1f5b2a22cf76a46965c47aeb7301e03e0c997c8c..e6c26179132205f9028779dc0a8d7868b9271f43 100644 (file)
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -949,6 +949,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
         match self#currentCicUri with
         | Some uri -> self#load (`Metadata (`Deps (`Back, uri)))
         | None -> ());
+      connect_menu_item win#browserCloseMenuItem (fun () ->
+        let my_id = Oo.id self in
+        cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers;
+        win#toplevel#misc#hide(); win#toplevel#destroy ());
       (* remove hbugs *)
       (*
       connect_menu_item win#hBugsTutorsMenuItem (fun () ->
@@ -1124,7 +1128,15 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
     method private tex () =
       let text = String.concat "\n"
-        (List.map (fun (k,vs) -> k ^ "\t" ^ String.concat ",  " vs)
+        (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