Semantic analysis implemented (sort of).

[helm.git] / helm / software / matita / matita.glade

diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade
index 0eaaaa7800e8a8e2bcb5aba2bfcf4258b05813b9..8cd2a9a73cbb97b689806045d2efb30d09c948a8 100644 (file)
--- a/helm/software/matita/matita.glade
+++ b/helm/software/matita/matita.glade
@@ -1180,6 +1180,14 @@
                                 </child>
                               </widget>
                             </child>
+                            <child>
+                              <widget class="GtkImageMenuItem" 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="use_underline">True</property>
+                              </widget>
+                            </child>
                           </widget>
                         </child>
                       </widget>
@@ -1222,6 +1230,14 @@
                                 </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>