83 |
extern void editor_init(void); |
extern void editor_init(void); |
84 |
extern void open_file_in_editor(GtkWidget *Editor, |
extern void open_file_in_editor(GtkWidget *Editor, |
85 |
const gchar *Filename, gint CurrentPage); |
const gchar *Filename, gint CurrentPage); |
|
extern void refresh_editor(GtkWidget *Editor, gint tos); |
|
86 |
|
|
87 |
gboolean catch_mult_line_indents (GtkWidget *widget, GdkEventKey *event, gpointer data); |
gboolean catch_mult_line_indents (GtkWidget *widget, GdkEventKey *event, gpointer data); |
88 |
|
|
89 |
void auto_indent_on_insert (GtkTextBuffer *Buffer, GtkTextIter *iter, gchar *text, |
void set_mime_type (gint page, gchar *mime_type); |
|
gint size, gpointer data); |
|
|
void auto_unindent_on_insert (GtkTextBuffer *Buffer, GtkTextIter *iter, gchar *text, |
|
|
gint size, gpointer data); |
|
|
|
|
90 |
|
|
91 |
#endif /* !__EDITOR_H__ */ |
#endif /* !__EDITOR_H__ */ |