X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatita.glade;h=0d80fe22c933960827789de606e3c3601b392610;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=11a7321d6e7a39cbb200a6b01b146916c0050f92;hpb=e325b771a3283acdb371cdc6f1f1929c0a0db3a1;p=helm.git

diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade
index 11a7321d6..0d80fe22c 100644
--- a/helm/software/matita/matita.glade
+++ b/helm/software/matita/matita.glade
@@ -1283,6 +1283,14 @@
                                 <property name="use_underline">True</property>
                               </widget>
                             </child>
+                            <child>
+                              <widget class="GtkMenuItem" id="showHintsDbMenuItem">
+                                <property name="visible">True</property>
+                                <property name="tooltip" translatable="yes">Displays the database of hints</property>
+                                <property name="label" translatable="yes">Hints database</property>
+                                <property name="use_underline">True</property>
+                              </widget>
+                            </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="showAutoGuiMenuItem">
                                 <property name="visible">True</property>
@@ -1307,8 +1315,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">
@@ -1417,8 +1425,14 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Implication (⇒_i)</property>
                                             <property name="response_id">0</property>
+                                            <child>
+                                              <widget class="GtkLabel" id="label8">
+                                                <property name="visible">True</property>
+                                                <property name="label" translatable="yes">Implication (⇒&lt;sub&gt;i&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </widget>
+                                            </child>
                                           </widget>
                                         </child>
                                         <child>
@@ -1426,8 +1440,14 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Conjunction (∧_i)</property>
                                             <property name="response_id">0</property>
+                                            <child>
+                                              <widget class="GtkLabel" id="label7">
+                                                <property name="visible">True</property>
+                                                <property name="label" translatable="yes">Conjunction (∧&lt;sub&gt;i&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </widget>
+                                            </child>
                                           </widget>
                                           <packing>
                                             <property name="position">1</property>
@@ -1438,8 +1458,14 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Disjunction left (∨_i_l)</property>
                                             <property name="response_id">0</property>
+                                            <child>
+                                              <widget class="GtkLabel" id="label9">
+                                                <property name="visible">True</property>
+                                                <property name="label" translatable="yes">Disjunction left (∨&lt;sub&gt;i-l&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </widget>
+                                            </child>
                                           </widget>
                                           <packing>
                                             <property name="position">2</property>
@@ -1450,8 +1476,14 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Disjunction right (∨_i_r)</property>
                                             <property name="response_id">0</property>
+                                            <child>
+                                              <widget class="GtkLabel" id="label10">
+                                                <property name="visible">True</property>
+                                                <property name="label" translatable="yes">Disjunction right (∨&lt;sub&gt;i-r&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </widget>
+                                            </child>
                                           </widget>
                                           <packing>
                                             <property name="position">3</property>
@@ -1462,8 +1494,14 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Negation (¬_i)</property>
                                             <property name="response_id">0</property>
+                                            <child>
+                                              <widget class="GtkLabel" id="label11">
+                                                <property name="visible">True</property>
+                                                <property name="label" translatable="yes">Negation (¬&lt;sub&gt;i&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </widget>
+                                            </child>
                                           </widget>
                                           <packing>
                                             <property name="position">4</property>
@@ -1474,8 +1512,14 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Top (⊤_i)</property>
                                             <property name="response_id">0</property>
+                                            <child>
+                                              <widget class="GtkLabel" id="label12">
+                                                <property name="visible">True</property>
+                                                <property name="label" translatable="yes">Top (⊤&lt;sub&gt;i&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </widget>
+                                            </child>
                                           </widget>
                                           <packing>
                                             <property name="position">5</property>
@@ -1486,8 +1530,14 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Universal (∀_i)</property>
                                             <property name="response_id">0</property>
+                                            <child>
+                                              <widget class="GtkLabel" id="label20">
+                                                <property name="visible">True</property>
+                                                <property name="label" translatable="yes">Universal (∀&lt;sub&gt;i&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </widget>
+                                            </child>
                                           </widget>
                                           <packing>
                                             <property name="position">6</property>
@@ -1498,8 +1548,14 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Existential (∃_i)</property>
                                             <property name="response_id">0</property>
+                                            <child>
+                                              <widget class="GtkLabel" id="label21">
+                                                <property name="visible">True</property>
+                                                <property name="label" translatable="yes">Existential (∃&lt;sub&gt;i&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </widget>
+                                            </child>
                                           </widget>
                                           <packing>
                                             <property name="position">7</property>
@@ -1533,8 +1589,14 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Implication (⇒_e)</property>
                                             <property name="response_id">0</property>
+                                            <child>
+                                              <widget class="GtkLabel" id="label22">
+                                                <property name="visible">True</property>
+                                                <property name="label" translatable="yes">Implication (⇒&lt;sub&gt;e&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </widget>
+                                            </child>
                                           </widget>
                                         </child>
                                         <child>
@@ -1542,8 +1604,14 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Conjunction left (∧_e_l)</property>
                                             <property name="response_id">0</property>
+                                            <child>
+                                              <widget class="GtkLabel" id="label23">
+                                                <property name="visible">True</property>
+                                                <property name="label" translatable="yes">Conjunction left (∧&lt;sub&gt;e-l&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </widget>
+                                            </child>
                                           </widget>
                                           <packing>
                                             <property name="position">1</property>
@@ -1554,8 +1622,14 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Conjunction right (∧_e_r)</property>
                                             <property name="response_id">0</property>
+                                            <child>
+                                              <widget class="GtkLabel" id="label24">
+                                                <property name="visible">True</property>
+                                                <property name="label" translatable="yes">Conjunction right (∧&lt;sub&gt;e-r&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </widget>
+                                            </child>
                                           </widget>
                                           <packing>
                                             <property name="position">2</property>
@@ -1566,8 +1640,14 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Disjunction (∨_e)</property>
                                             <property name="response_id">0</property>
+                                            <child>
+                                              <widget class="GtkLabel" id="label27">
+                                                <property name="visible">True</property>
+                                                <property name="label" translatable="yes">Disjunction (∨&lt;sub&gt;e&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </widget>
+                                            </child>
                                           </widget>
                                           <packing>
                                             <property name="position">3</property>
@@ -1578,8 +1658,14 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Negation (¬_e)</property>
                                             <property name="response_id">0</property>
+                                            <child>
+                                              <widget class="GtkLabel" id="label31">
+                                                <property name="visible">True</property>
+                                                <property name="label" translatable="yes">Negation (¬&lt;sub&gt;e&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </widget>
+                                            </child>
                                           </widget>
                                           <packing>
                                             <property name="position">4</property>
@@ -1590,8 +1676,14 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Bottom (⊥_e)</property>
                                             <property name="response_id">0</property>
+                                            <child>
+                                              <widget class="GtkLabel" id="label33">
+                                                <property name="visible">True</property>
+                                                <property name="label" translatable="yes">Bottom (⊥&lt;sub&gt;e&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </widget>
+                                            </child>
                                           </widget>
                                           <packing>
                                             <property name="position">5</property>
@@ -1602,8 +1694,14 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Universal (∀_e)</property>
                                             <property name="response_id">0</property>
+                                            <child>
+                                              <widget class="GtkLabel" id="label34">
+                                                <property name="visible">True</property>
+                                                <property name="label" translatable="yes">Universal (∀&lt;sub&gt;e&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </widget>
+                                            </child>
                                           </widget>
                                           <packing>
                                             <property name="position">6</property>
@@ -1614,8 +1712,14 @@
                                             <property name="visible">True</property>
                                             <property name="can_focus">True</property>
                                             <property name="receives_default">True</property>
-                                            <property name="label" translatable="yes">Existential (∃_e)</property>
                                             <property name="response_id">0</property>
+                                            <child>
+                                              <widget class="GtkLabel" id="label35">
+                                                <property name="visible">True</property>
+                                                <property name="label" translatable="yes">Existential (∃&lt;sub&gt;e&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </widget>
+                                            </child>
                                           </widget>
                                           <packing>
                                             <property name="position">7</property>