]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/DEVEL/mathml_editor/test/guiGTK.c
* changed handling of ' (\primes) with a few patches in the stylesheets
[helm.git] / helm / DEVEL / mathml_editor / test / guiGTK.c
index 7426e3f5db0da0ed6b629e8820fe46b0e192e9e3..74a34608b6da86decca8acbfd30e21e09a5b11a3 100644 (file)
@@ -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>" },
@@ -133,6 +137,9 @@ load_error_msg(const char* name)
   g_free(msg);
 }
 
+static guint edit_timeout_id;
+extern void edit_timeout(gpointer);
+
 void
 GUI_init(int* argc, char*** argv, char* title, guint width, guint height, gpointer c)
 {
@@ -147,7 +154,7 @@ GUI_init(int* argc, char*** argv, char* title, guint width, guint height, gpoint
   gtk_widget_show(window);
 
   context = c;
-  /*edit_timeout_id = gtk_timeout_add(400, edit_timeout, context);*/
+  /*edit_timeout_id = gtk_timeout_add(50, edit_timeout, context);*/
 }
 
 void
@@ -298,6 +305,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 +383,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)
 {