X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FDEVEL%2Fmathml_editor%2Ftest%2FguiGTK.c;h=306ec67facf52439422a7797db4c85984c9153bb;hb=1957a1f151c547f04625c4379e51ab66bddb69c7;hp=7426e3f5db0da0ed6b629e8820fe46b0e192e9e3;hpb=387aeebf96181c051b7f527a0901b173cfcdf194;p=helm.git

diff --git a/helm/DEVEL/mathml_editor/test/guiGTK.c b/helm/DEVEL/mathml_editor/test/guiGTK.c
index 7426e3f5d..306ec67fa 100644
--- a/helm/DEVEL/mathml_editor/test/guiGTK.c
+++ b/helm/DEVEL/mathml_editor/test/guiGTK.c
@@ -48,6 +48,7 @@ static GtkWidget* get_main_menu(void);
 static void file_open(GtkWidget*, gpointer);
 static void file_re_open(GtkWidget*, gpointer);
 static void file_close(GtkWidget*, gpointer);
+static void file_output_tex(GtkWidget*, gpointer);
 static void options_font_manager(GtkWidget*, FontManagerId);
 static void options_set_font_size(GtkWidget*, gpointer);
 static void options_change_font_size(GtkWidget*, gboolean);
@@ -57,6 +58,7 @@ static void options_transparency(GtkWidget*, gpointer);
 static void edit_delete_selection(GtkWidget*, gpointer);
 static void edit_select_parent(GtkWidget*, gpointer);
 static void edit_reset_selection(GtkWidget*, gpointer);
+static void edit_reset(GtkWidget*, gpointer);
 static void edit_insert(GtkWidget*, gpointer);
 static void help_about(GtkWidget*, gpointer);
 
@@ -65,6 +67,7 @@ static GtkItemFactoryEntry menu_items[] = {
   { "/File/_Open...",                  "<control>O", file_open,     0, NULL },
   { "/File/_Reopen",                   NULL,         file_re_open,  0, NULL },
   { "/File/_Close",                    "<control>W", file_close,    0, NULL },
+  { "/File/Output _TeX",               NULL,         file_output_tex, 0, NULL },
   { "/File/sep1",                      NULL,         NULL,          0, "<Separator>" },
   { "/File/_Quit",                     "<control>Q", gtk_main_quit, 0, NULL },
 
@@ -73,6 +76,7 @@ static GtkItemFactoryEntry menu_items[] = {
   { "/Edit/Delete Selection",          NULL, edit_delete_selection, 0, NULL },
   { "/Edit/Select Parent",             NULL, edit_select_parent,    0, NULL },
   { "/Edit/sep1",                      NULL,         NULL,          0, "<Separator>" },
+  { "/Edit/_Reset",                    NULL, edit_reset,            0, NULL },
   { "/Edit/Insert...",                 "<control>I", edit_insert,   0, NULL },
 
   { "/_Options",                       NULL, NULL,                  0,  "<Branch>" },
@@ -298,6 +302,13 @@ file_open(GtkWidget* widget, gpointer data)
   gtk_widget_show (fs);
 }
 
+static void
+file_output_tex(GtkWidget* widget, gpointer data)
+{
+  g_assert(context != NULL);
+  edit_output_tex(context);
+}
+
 static void
 options_font_manager(GtkWidget* widget, FontManagerId id)
 {
@@ -369,6 +380,13 @@ edit_reset_selection(GtkWidget* widget, gpointer data)
     }
 }
 
+static void
+edit_reset(GtkWidget* widget, gpointer data)
+{
+  g_assert(context != NULL);
+  edit_reset_tex(context);
+}
+
 static void
 insert_tex(GtkWidget* widget, GtkEntry* entry)
 {