X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FDEVEL%2Fmathml_editor%2Ftest%2FguiGTK.c;h=cf59421cffecbdc2f92b6db7d99218e32798490d;hb=bf6bbd9f2e47ce7a465c0bb3105f9a7c7d73a9ea;hp=1bcf786ad1852c3364acc68613ea1b9ad49c55d1;hpb=c112706f347e08e7f345131fbc4c3aa0e9ecc7b5;p=helm.git

diff --git a/helm/DEVEL/mathml_editor/test/guiGTK.c b/helm/DEVEL/mathml_editor/test/guiGTK.c
index 1bcf786ad..cf59421cf 100644
--- a/helm/DEVEL/mathml_editor/test/guiGTK.c
+++ b/helm/DEVEL/mathml_editor/test/guiGTK.c
@@ -28,7 +28,7 @@
 #include <gtk/gtk.h>
 #include <gdk/gdkkeysyms.h>
 
-#include <gtkmathview/gtkmathview.h>
+#include <gtkmathview.h>
 #include "guiGTK.h"
 
 #define XLINK_NS_URI "http://www.w3.org/1999/xlink"
@@ -50,7 +50,6 @@ 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);
 static void options_verbosity(GtkWidget*, guint);
@@ -86,9 +85,6 @@ static GtkItemFactoryEntry menu_items[] = {
   { "/Options/Default Font Size/sep1", NULL, NULL,                  0,  "<Separator>" },
   { "/Options/Default Font Size/Larger", NULL, options_change_font_size, TRUE, NULL },
   { "/Options/Default Font Size/Smaller", NULL, options_change_font_size, FALSE, NULL },
-  { "/Options/Font Manager",           NULL, NULL,                  0,  "<Branch>" },
-  { "/Options/Font Manager/_GTK",      NULL, options_font_manager,  FONT_MANAGER_GTK, "<RadioItem>" },
-  { "/Options/Font Manager/_Type 1",   NULL, options_font_manager,  FONT_MANAGER_T1, "/Options/Font Manager/GTK" },
   { "/Options/Verbosity",              NULL, NULL,                  0,  "<Branch>" },
   { "/Options/Verbosity/_Errors",      NULL, options_verbosity,     0,  "<RadioItem>" },
   { "/Options/Verbosity/_Warnings",    NULL, options_verbosity,     1,  "/Options/Verbosity/Errors" },
@@ -230,6 +226,7 @@ GUI_run()
   gtk_main();
 }
 
+#if 0
 void
 GUI_set_font_manager(FontManagerId id)
 {
@@ -260,6 +257,7 @@ GUI_set_font_manager(FontManagerId id)
 
   gtk_math_view_thaw(math_view);
 }
+#endif
 
 static void
 store_filename(GtkFileSelection* selector, GtkWidget* user_data)
@@ -313,12 +311,14 @@ file_output_tex(GtkWidget* widget, gpointer data)
   edit_output_tex(context);
 }
 
+#if 0
 static void
 options_font_manager(GtkWidget* widget, FontManagerId id)
 {
   g_return_if_fail(id != FONT_MANAGER_UNKNOWN);
   GUI_set_font_manager(id);
 }
+#endif
 
 static void
 options_anti_aliasing(GtkWidget* widget, gpointer data)
@@ -596,10 +596,13 @@ key_press_event(gpointer c,
   switch (event->keyval)
     {
     case GDK_BackSpace:
-      edit_drop(context, event->state & GDK_MOD1_MASK);
+      edit_drop(context, event->state & GDK_MOD1_MASK, event->state & GDK_CONTROL_MASK);
+      break;
+    case GDK_Tab:
+      edit_complete(context);
       break;
     default:
-      if ((event->state & (~GDK_SHIFT_MASK)) == 0 && event->keyval < 0x80)
+      if ((event->state & (GDK_CONTROL_MASK | GDK_MOD1_MASK)) == 0 && event->keyval < 0x80)
 	edit_push_char(context, event->keyval);
       return FALSE;
     }