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

diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade
index a14858d91..0d80fe22c 100644
--- a/helm/software/matita/matita.glade
+++ b/helm/software/matita/matita.glade
@@ -1022,6 +1022,15 @@
                                 <property name="use_underline">True</property>
                               </widget>
                             </child>
+                            <child>
+                              <widget class="GtkCheckMenuItem" id="menuitemAutoAltL">
+                                <property name="visible">True</property>
+                                <property name="tooltip" translatable="yes">Automatically expands TeX macros to their corresponding UTF-8 symbol</property>
+                                <property name="label" translatable="yes">Auto-expand TeX Macros</property>
+                                <property name="use_underline">True</property>
+                                <property name="active">True</property>
+                              </widget>
+                            </child>
                             <child>
                               <widget class="GtkImageMenuItem" id="deleteMenuItem">
                                 <property name="visible">True</property>
@@ -1274,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>
@@ -1298,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">
@@ -1408,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>
@@ -1417,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>
@@ -1429,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>
@@ -1441,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>
@@ -1453,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>
@@ -1465,13 +1512,55 @@
                                             <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>
                                           </packing>
                                         </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butForall_intro">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</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>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butExists_intro">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</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>
+                                          </packing>
+                                        </child>
                                       </widget>
                                     </child>
                                     <child>
@@ -1500,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>
@@ -1509,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>
@@ -1521,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>
@@ -1533,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>
@@ -1545,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>
@@ -1557,13 +1676,55 @@
                                             <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>
                                           </packing>
                                         </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butForall_elim">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</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>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butExists_elim">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</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>
+                                          </packing>
+                                        </child>
                                       </widget>
                                     </child>
                                     <child>
@@ -2350,6 +2511,59 @@
         <property name="n_rows">3</property>
         <property name="n_columns">2</property>
         <property name="row_spacing">5</property>
+        <child>
+          <widget class="GtkLabel" id="label17">
+            <property name="visible">True</property>
+            <property name="xalign">0</property>
+            <property name="label" translatable="yes">Find:</property>
+          </widget>
+          <packing>
+            <property name="x_options"></property>
+            <property name="y_options"></property>
+          </packing>
+        </child>
+        <child>
+          <widget class="GtkLabel" id="label18">
+            <property name="visible">True</property>
+            <property name="xalign">0</property>
+            <property name="label" translatable="yes">Replace with: </property>
+          </widget>
+          <packing>
+            <property name="top_attach">1</property>
+            <property name="bottom_attach">2</property>
+            <property name="x_options"></property>
+            <property name="y_options"></property>
+          </packing>
+        </child>
+        <child>
+          <widget class="GtkEntry" id="findEntry">
+            <property name="visible">True</property>
+            <property name="can_focus">True</property>
+            <property name="has_focus">True</property>
+            <property name="can_default">True</property>
+            <property name="has_default">True</property>
+            <property name="invisible_char">*</property>
+          </widget>
+          <packing>
+            <property name="left_attach">1</property>
+            <property name="right_attach">2</property>
+            <property name="y_options"></property>
+          </packing>
+        </child>
+        <child>
+          <widget class="GtkEntry" id="replaceEntry">
+            <property name="visible">True</property>
+            <property name="can_focus">True</property>
+            <property name="invisible_char">*</property>
+          </widget>
+          <packing>
+            <property name="left_attach">1</property>
+            <property name="right_attach">2</property>
+            <property name="top_attach">1</property>
+            <property name="bottom_attach">2</property>
+            <property name="y_options"></property>
+          </packing>
+        </child>
         <child>
           <widget class="GtkHBox" id="hbox19">
             <property name="visible">True</property>
@@ -2448,59 +2662,6 @@
             <property name="y_padding">5</property>
           </packing>
         </child>
-        <child>
-          <widget class="GtkEntry" id="replaceEntry">
-            <property name="visible">True</property>
-            <property name="can_focus">True</property>
-            <property name="invisible_char">*</property>
-          </widget>
-          <packing>
-            <property name="left_attach">1</property>
-            <property name="right_attach">2</property>
-            <property name="top_attach">1</property>
-            <property name="bottom_attach">2</property>
-            <property name="y_options"></property>
-          </packing>
-        </child>
-        <child>
-          <widget class="GtkEntry" id="findEntry">
-            <property name="visible">True</property>
-            <property name="can_focus">True</property>
-            <property name="has_focus">True</property>
-            <property name="can_default">True</property>
-            <property name="has_default">True</property>
-            <property name="invisible_char">*</property>
-          </widget>
-          <packing>
-            <property name="left_attach">1</property>
-            <property name="right_attach">2</property>
-            <property name="y_options"></property>
-          </packing>
-        </child>
-        <child>
-          <widget class="GtkLabel" id="label18">
-            <property name="visible">True</property>
-            <property name="xalign">0</property>
-            <property name="label" translatable="yes">Replace with: </property>
-          </widget>
-          <packing>
-            <property name="top_attach">1</property>
-            <property name="bottom_attach">2</property>
-            <property name="x_options"></property>
-            <property name="y_options"></property>
-          </packing>
-        </child>
-        <child>
-          <widget class="GtkLabel" id="label17">
-            <property name="visible">True</property>
-            <property name="xalign">0</property>
-            <property name="label" translatable="yes">Find:</property>
-          </widget>
-          <packing>
-            <property name="x_options"></property>
-            <property name="y_options"></property>
-          </packing>
-        </child>
       </widget>
     </child>
   </widget>