]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/DEVEL/mathml_editor/test/guiGTK.c
* snapshot for gtk2
[helm.git] / helm / DEVEL / mathml_editor / test / guiGTK.c
index 01994eaf148cce7fcd4ed8704113f7175e2dca73..cf59421cffecbdc2f92b6db7d99218e32798490d 100644 (file)
@@ -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)