From: Stefano Zacchiroli Date: Fri, 10 Jun 2005 11:38:53 +0000 (+0000) Subject: snaphot X-Git-Tag: PRE_STORAGE~86 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c0f566c371cefef7666a6d68dd1b6c38ca6918ce;p=helm.git snaphot - better creation of GtkSourceView (using C constructor) - bound GtkSourceLanguage - preliminary binding of GtkSourceLanguagesManager --- diff --git a/helm/DEVEL/lablgtksourceview/gSourceView.ml b/helm/DEVEL/lablgtksourceview/gSourceView.ml index 30f13b2fe..a6b34aa9f 100644 --- a/helm/DEVEL/lablgtksourceview/gSourceView.ml +++ b/helm/DEVEL/lablgtksourceview/gSourceView.ml @@ -32,19 +32,39 @@ open GtkSourceView open OgtkSourceViewProps open GObj -let get_bool = function `BOOL b -> b | _ -> assert false -let bool b = `BOOL b -let get_uint = function `INT i -> i | _ -> assert false -let uint i = `INT i -let get_int = function `INT i -> i | _ -> assert false -let int i = `INT i +let get_bool = function `BOOL x -> x | _ -> assert false +let bool x = `BOOL x +let get_uint = function `INT x -> x | _ -> assert false +let uint x = `INT x +let get_int = function `INT x -> x | _ -> assert false +let int x = `INT x +let get_gobject = function `OBJECT x -> x | _ -> assert false +let gobject x = `OBJECT (Some x) + +(** {2 GtkSourceLanguage} *) + +class source_language_signals obj' = +object (self) + inherit ['a] gobject_signals (obj' : [> Gtk_sourceview.source_language] obj) + inherit source_language_sigs +end + +class source_language (obj: Gtk_sourceview.source_language obj) = +object (self) + method as_source_language = obj + method connect = new source_language_signals obj + method misc = new gobject_ops obj + method get_name = SourceLanguage.get_name obj + method get_section = SourceLanguage.get_section obj + method get_escape_char = SourceLanguage.get_escape_char obj +end (** {2 GtkSourceBuffer} *) -class source_buffer_signals obj_arg = +class source_buffer_signals obj' = object - inherit ['a] gobject_signals (obj_arg : [> Gtk_sourceview.source_buffer] obj) - inherit GText.buffer_signals obj_arg + inherit ['a] gobject_signals (obj' : [> Gtk_sourceview.source_buffer] obj) + inherit GText.buffer_signals obj' inherit source_buffer_sigs end @@ -60,6 +80,13 @@ object (self) method max_undo_levels = get_int (self#misc#get_property "max-undo-levels") method set_max_undo_levels x = self#misc#set_property "max-undo-levels" (int x) + method language = + match get_gobject (self#misc#get_property "language") with + | None -> None + | Some obj -> + Some (new source_language (Gobject.try_cast obj "GtkSourceLanguage")) + method set_language (x: source_language) = + self#misc#set_property "language" (gobject x#as_source_language) method escape_char = get_uint (self#misc#get_property "escape-char") method set_escape_char x = self#misc#set_property "escape-char" (uint x) method can_undo = SourceBuffer.can_undo obj @@ -72,8 +99,13 @@ object (self) SourceBuffer.end_not_undoable_action obj end -let source_buffer ?text = - SourceBuffer.make_params [] ~cont:(fun pl () -> +let source_buffer ?language ?text (* ?tag_table *) = + let language = + match language with + | None -> None + | Some source_language -> Some (source_language#as_source_language) + in + SourceBuffer.make_params [] ?language ~cont:(fun pl () -> let buf = new source_buffer (SourceBuffer.create pl) in (match text with | None -> () @@ -85,17 +117,23 @@ let source_buffer' = source_buffer (** {2 GtkSourceView} *) -class source_view_signals obj_arg = +class source_view_signals obj' = object - inherit widget_signals_impl (obj_arg : [> Gtk_sourceview.source_view] obj) - inherit GText.view_signals obj_arg + inherit widget_signals_impl (obj' : [> Gtk_sourceview.source_view] obj) + inherit GText.view_signals obj' inherit source_view_sigs end -class source_view (obj: Gtk_sourceview.source_view obj) = +class source_view (obj': Gtk_sourceview.source_view obj) = object (self) - inherit GText.view_skel obj - method connect = new source_view_signals obj + inherit GText.view_skel obj' + val source_buf = + let buf_obj = + Gobject.try_cast (GtkText.View.get_buffer obj') "GtkSourceBuffer" + in + new source_buffer buf_obj + method source_buffer = source_buf + method connect = new source_view_signals obj' method set_show_line_numbers x = self#misc#set_property "show_line_numbers" (bool x) method show_line_numbers = @@ -124,12 +162,13 @@ let source_view ?source_buffer = SourceView.make_params [] ~cont:( GtkText.View.make_params ~cont:( GContainer.pack_container ~create:(fun pl -> - let buf = + let obj = match source_buffer with - | None -> source_buffer' () - | Some source_buffer -> source_buffer + | Some buf -> + SourceView.new_with_buffer + (Gobject.try_cast buf#as_buffer "GtkSourceBuffer") + | None -> SourceView.new_ () in - let obj = SourceView.create pl in - GtkText.View.set_buffer obj buf#as_buffer; + Gobject.set_params (Gobject.try_cast obj "GtkSourceView") pl; new source_view obj))) diff --git a/helm/DEVEL/lablgtksourceview/gSourceView.mli b/helm/DEVEL/lablgtksourceview/gSourceView.mli index a041f28a8..f933cf610 100644 --- a/helm/DEVEL/lablgtksourceview/gSourceView.mli +++ b/helm/DEVEL/lablgtksourceview/gSourceView.mli @@ -25,44 +25,41 @@ open Gtk +(** {2 GtkSourceLanguage} *) + +class source_language_signals: + ([> Gtk_sourceview.source_language ] as 'b) obj -> + object ('a) + inherit ['b] GObj.gobject_signals + method tag_style_changed: callback:(string -> unit) -> GtkSignal.id + end + +class source_language: + Gtk_sourceview.source_language obj -> + object + method as_source_language: Gtk_sourceview.source_language obj + method connect: source_language_signals + method get_escape_char: Glib.unichar + method get_name: string + method get_section: string + method misc: GObj.gobject_ops + end + (** {2 GtkSourceBuffer} *) class source_buffer_signals: ([> Gtk_sourceview.source_buffer ] as 'b) obj -> object ('a) - method after : 'a - method apply_tag : - callback:(GText.tag -> start:GText.iter -> stop:GText.iter -> unit) -> - GtkSignal.id - method begin_user_action : callback:(unit -> unit) -> GtkSignal.id - method can_redo : callback:(bool -> unit) -> GtkSignal.id - method can_undo : callback:(bool -> unit) -> GtkSignal.id - method changed : callback:(unit -> unit) -> GtkSignal.id - method private connect : - 'c. ('b, 'c) GtkSignal.t -> callback:'c -> GtkSignal.id - method delete_range : - callback:(start:GText.iter -> stop:GText.iter -> unit) -> GtkSignal.id - method end_user_action : callback:(unit -> unit) -> GtkSignal.id - method highlight_updated : + inherit GText.buffer_signals + method can_redo: callback:(bool -> unit) -> GtkSignal.id + method can_undo: callback:(bool -> unit) -> GtkSignal.id + method highlight_updated: callback:(Gtk.text_iter -> Gtk.text_iter -> unit) -> GtkSignal.id - method insert_child_anchor : - callback:(GText.iter -> Gtk.text_child_anchor -> unit) -> GtkSignal.id - method insert_pixbuf : - callback:(GText.iter -> GdkPixbuf.pixbuf -> unit) -> GtkSignal.id - method insert_text : - callback:(GText.iter -> string -> unit) -> GtkSignal.id - method mark_deleted : callback:(Gtk.text_mark -> unit) -> GtkSignal.id - method mark_set : - callback:(GText.iter -> Gtk.text_mark -> unit) -> GtkSignal.id - method marker_updated : callback:(Gtk.text_iter -> unit) -> GtkSignal.id - method modified_changed : callback:(unit -> unit) -> GtkSignal.id - method remove_tag : - callback:(GText.tag -> start:GText.iter -> stop:GText.iter -> unit) -> - GtkSignal.id + method marker_updated: callback:(Gtk.text_iter -> unit) -> GtkSignal.id end class source_buffer: - Gtk_sourceview.source_buffer Gtk.obj -> + Gtk_sourceview.source_buffer obj -> object inherit GText.buffer_skel method connect: source_buffer_signals @@ -74,8 +71,8 @@ class source_buffer: method set_highlight: bool -> unit method max_undo_levels: int method set_max_undo_levels: int -> unit -(* method language: source_language *) -(* method set_language: source_language -> unit *) + method language: source_language option + method set_language: source_language -> unit method escape_char: Glib.unichar method set_escape_char: Glib.unichar -> unit method can_undo: bool @@ -97,56 +94,38 @@ class source_buffer: (* method get_prev_marker: unit -> source_marker *) end -val source_buffer : +val source_buffer: + ?language:source_language -> +(* ?tag_table:source_tag_table -> *) ?text:string -> ?check_brackets:bool -> ?escape_char:int -> ?highlight:bool -> ?max_undo_levels:int -> -(* ?tag_table:GText.tag_table -> *) unit -> source_buffer (** {2 GtkSourceView} *) -class source_view_signals : +class source_view_signals: ([> Gtk_sourceview.source_view ] as 'b) obj -> object ('a) - method after : 'a - method copy_clipboard : callback:(unit -> unit) -> GtkSignal.id - method cut_clipboard : callback:(unit -> unit) -> GtkSignal.id - method delete_from_cursor : - callback:(Gtk.Tags.delete_type -> int -> unit) -> GtkSignal.id - method destroy : callback:(unit -> unit) -> GtkSignal.id - method insert_at_cursor : callback:(string -> unit) -> GtkSignal.id - method move_cursor : - callback:(Gtk.Tags.movement_step -> int -> extend:bool -> unit) -> - GtkSignal.id - method move_focus : - callback:(Gtk.Tags.direction_type -> unit) -> GtkSignal.id - method page_horizontally : - callback:(int -> extend:bool -> unit) -> GtkSignal.id - method paste_clipboard : callback:(unit -> unit) -> GtkSignal.id - method populate_popup : - callback:(Gtk.menu Gtk.obj -> unit) -> GtkSignal.id - method redo : callback:(unit -> unit) -> GtkSignal.id - method set_anchor : callback:(unit -> unit) -> GtkSignal.id - method set_scroll_adjustments : - callback:(GData.adjustment option -> GData.adjustment option -> unit) -> GtkSignal.id - method toggle_overwrite : callback:(unit -> unit) -> GtkSignal.id - method undo : callback:(unit -> unit) -> GtkSignal.id + inherit GText.view_signals + method redo: callback:(unit -> unit) -> GtkSignal.id + method undo: callback:(unit -> unit) -> GtkSignal.id end -class source_view : - Gtk_sourceview.source_view Gtk.obj -> +class source_view: + Gtk_sourceview.source_view obj -> object inherit GText.view_skel - val obj: Gtk_sourceview.source_view Gtk.obj + val obj: Gtk_sourceview.source_view obj method connect: source_view_signals - method set_show_line_numbers : bool -> unit - method show_line_numbers : bool - method set_show_line_markers : bool -> unit - method show_line_markers : bool + method source_buffer: source_buffer + method set_show_line_numbers: bool -> unit + method show_line_numbers: bool + method set_show_line_markers: bool -> unit + method show_line_markers: bool method set_tabs_width: int -> unit method tabs_width: int method set_auto_indent: bool -> unit @@ -163,7 +142,7 @@ class source_view : method smart_home_end: bool end -val source_view : +val source_view: ?source_buffer:source_buffer -> ?auto_indent:bool -> ?insert_spaces_instead_of_tabs:bool -> diff --git a/helm/DEVEL/lablgtksourceview/gtkSourceView.ml b/helm/DEVEL/lablgtksourceview/gtkSourceView.ml index 87745712e..79d448b02 100644 --- a/helm/DEVEL/lablgtksourceview/gtkSourceView.ml +++ b/helm/DEVEL/lablgtksourceview/gtkSourceView.ml @@ -31,21 +31,59 @@ open Tags open GtkSourceViewProps open GtkBase -external _gtk_source_view_init : unit -> unit = "ml_gtk_source_view_init" -external _gtk_source_buffer_init : unit -> unit = "ml_gtk_source_buffer_init" +external _gtk_source_language_init: unit -> unit = "ml_gtk_source_language_init" +external _gtk_source_languages_manager_init: unit -> unit = + "ml_gtk_source_languages_manager_init" +external _gtk_source_buffer_init: unit -> unit = "ml_gtk_source_buffer_init" +external _gtk_source_view_init: unit -> unit = "ml_gtk_source_view_init" let () = - _gtk_source_view_init (); - _gtk_source_buffer_init () + _gtk_source_language_init (); + _gtk_source_languages_manager_init (); + _gtk_source_buffer_init (); + _gtk_source_view_init () -module SourceView = +module SourceLanguage = struct - include SourceView + include SourceLanguage + external get_name: [>`sourcelanguage] obj -> string = + "ml_gtk_source_language_get_name" + external get_section: [>`sourcelanguage] obj -> string = + "ml_gtk_source_language_get_section" +(* external get_tags: [>`sourcelanguage] obj -> source_tag list *) + external get_escape_char: [>`sourcelanguage] obj -> Glib.unichar = + "ml_gtk_source_language_get_escape_char" +(* external get_mime_types: [>`sourcelanguage] obj -> string list *) +(* external set_mime_types: [>`sourcelanguage] obj -> string list -> unit *) +(* external get_style_scheme: [>`sourcelanguage] obj -> style_scheme *) +(* external set_style_char: [>`sourcelanguage] obj -> style_scheme -> unit *) +(* external get_tag_style: [>`sourcelanguage] obj -> tag_style *) +(* external set_tag_style: [>`sourcelanguage] obj -> string -> tag_style -> unit *) +(* external get_tag_default_style: [>`sourcelanguage] obj -> string -> tag_style *) +end + +module SourceLanguagesManager = +struct + include SourceLanguagesManager + external new_: unit -> source_languages_manager obj = + "ml_gtk_source_languages_manager_new" +(* external get_available_languages: + [>`sourcelanguagesmanager] obj -> source_language obj list + = "ml_gtk_source_languages_manager_get_available_languages" *) + external get_language_from_mime_type: + [>`sourcelanguagesmanager] obj -> source_language obj + = "ml_gtk_source_languages_manager_get_language_from_mime_type" +(* external get_lang_files_dirs: + [>`sourcelanguagesmanager] obj -> string list + = "ml_gtk_source_languages_manager_get_lang_files_dirs" *) end module SourceBuffer = struct include SourceBuffer +(* external new_: unit -> source_buffer obj = "ml_gtk_source_buffer_new" *) +(* external new_with_buffer: [>`sourcelanguage] obj -> source_buffer obj = + "ml_gtk_source_buffer_new_with_language" *) external can_undo: [>`sourcebuffer] obj -> bool = "ml_gtk_source_buffer_can_undo" external can_redo: [>`sourcebuffer] obj -> bool = @@ -58,3 +96,11 @@ struct "ml_gtk_source_buffer_end_not_undoable_action" end +module SourceView = +struct + include SourceView + external new_: unit -> source_view obj = "ml_gtk_source_view_new" + external new_with_buffer: [>`sourcebuffer] obj -> source_view obj = + "ml_gtk_source_view_new_with_buffer" +end + diff --git a/helm/DEVEL/lablgtksourceview/gtkSourceView.props b/helm/DEVEL/lablgtksourceview/gtkSourceView.props index 25885c796..a8a6f6e93 100644 --- a/helm/DEVEL/lablgtksourceview/gtkSourceView.props +++ b/helm/DEVEL/lablgtksourceview/gtkSourceView.props @@ -5,17 +5,12 @@ header { open Gtk_sourceview } -class SourceView type "source_view obj" set wrapsig : Widget { - "auto-indent" gboolean : Read / Write - "insert-spaces-instead-of-tabs" gboolean : Read / Write - "margin" guint : Read / Write - "show-line-markers" gboolean : Read / Write - "show-line-numbers" gboolean : Read / Write - "show-margin" gboolean : Read / Write - "smart-home-end" gboolean : Read / Write - "tabs-width" guint : Read / Write - signal redo - signal undo +class SourceLanguage type "source_language obj" set wrapsig : GObject { + signal tag_style_changed: string +} + +class SourceLanguagesManager type "source_languages_manager obj" set wrapsig : GObject { +(* "lang-files-dirs" gpointer : Read / Write / Construct Only *) } class SourceBuffer type "source_buffer obj" set wrapsig : GObject { @@ -30,3 +25,16 @@ class SourceBuffer type "source_buffer obj" set wrapsig : GObject { signal marker_updated: GtkTextIter } +class SourceView type "source_view obj" set wrapsig : Widget { + "auto-indent" gboolean : Read / Write + "insert-spaces-instead-of-tabs" gboolean : Read / Write + "margin" guint : Read / Write + "show-line-markers" gboolean : Read / Write + "show-line-numbers" gboolean : Read / Write + "show-margin" gboolean : Read / Write + "smart-home-end" gboolean : Read / Write + "tabs-width" guint : Read / Write + signal redo + signal undo +} + diff --git a/helm/DEVEL/lablgtksourceview/gtk_sourceview.ml b/helm/DEVEL/lablgtksourceview/gtk_sourceview.ml index 8c1f6be6c..957db6d38 100644 --- a/helm/DEVEL/lablgtksourceview/gtk_sourceview.ml +++ b/helm/DEVEL/lablgtksourceview/gtk_sourceview.ml @@ -25,4 +25,6 @@ type source_view = [Gtk.text_view|`sourceview] type source_buffer = [Gtk.text_buffer|`sourcebuffer] +type source_language = [`sourcelanguage] +type source_languages_manager = [`sourcelanguagesmanager] diff --git a/helm/DEVEL/lablgtksourceview/ml_gtk_sourceview.c b/helm/DEVEL/lablgtksourceview/ml_gtk_sourceview.c index eb0a69dc5..f9b92dc1c 100644 --- a/helm/DEVEL/lablgtksourceview/ml_gtk_sourceview.c +++ b/helm/DEVEL/lablgtksourceview/ml_gtk_sourceview.c @@ -26,6 +26,7 @@ #include #include +#include #include #include @@ -47,9 +48,15 @@ /* Init all */ -CAMLprim value ml_gtk_source_view_init(value unit) +CAMLprim value ml_gtk_source_language_init(value unit) { /* Since these are declared const, must force gcc to call them! */ - GType t = gtk_source_view_get_type(); + GType t = gtk_source_language_get_type(); + return Val_GType(t); +} + +CAMLprim value ml_gtk_source_languages_manager_init(value unit) +{ /* Since these are declared const, must force gcc to call them! */ + GType t = gtk_source_languages_manager_get_type(); return Val_GType(t); } @@ -59,32 +66,30 @@ CAMLprim value ml_gtk_source_buffer_init(value unit) return Val_GType(t); } -#define GtkSourceView_val(val) check_cast(GTK_SOURCE_VIEW,val) -#define GtkSourceBuffer_val(val) check_cast(GTK_SOURCE_BUFFER,val) +CAMLprim value ml_gtk_source_view_init(value unit) +{ /* Since these are declared const, must force gcc to call them! */ + GType t = gtk_source_view_get_type(); + return Val_GType(t); +} -//##################################### -// -//#define FontManagerId_val(val) Int_val(val) -//#define Val_FontManagerId(val) Val_int(val) -// -///* As ML_1, but the result is optional */ -//#define OML_1(cname, conv1, conv) \ -//value ml_##cname (value arg1) { return Val_option_ptr((cname (conv1 (arg1))),conv); } -///* As ML_3, but the result is optional */ -//#define OML_3(cname, conv1, conv2, conv3, conv) \ -value ml_##cname (value arg1, value arg2, value arg3) { return Val_option_ptr((cname (conv1 (arg1), conv2 (arg2), conv3 (arg3))),conv); } -///* As ML_2, but the second argument is optional */ -//#define ML_2O(cname, conv1, conv2, conv) \ -//value ml_##cname (value arg1, value arg2) \ -//{ return conv (cname (conv1(arg1), ptr_val_option(arg2,conv2))); } +#define GtkSourceLanguage_val(val) check_cast(GTK_SOURCE_LANGUAGE,val) +#define GtkSourceLanguagesManager_val(val)\ + check_cast(GTK_SOURCE_LANGUAGES_MANAGER,val) +#define GtkSourceTagTable_val(val) check_cast(GTK_SOURCE_TAG_TABLE,val) +#define GtkSourceBuffer_val(val) check_cast(GTK_SOURCE_BUFFER,val) +#define GtkSourceView_val(val) check_cast(GTK_SOURCE_VIEW,val) -/* ML_1 (gtk_math_view_freeze, GtkMathView_val, Unit) -ML_2 (gtk_math_view_load_uri, GtkMathView_val, String_val, Val_bool) -ML_3 (gtk_math_view_set_top, GtkMathView_val, Int_val, Int_val, Unit) */ +ML_1 (gtk_source_language_get_name, GtkSourceLanguage_val, Val_string) +ML_1 (gtk_source_language_get_section, GtkSourceLanguage_val, Val_string) +ML_1 (gtk_source_language_get_escape_char, GtkSourceLanguage_val, Val_int) -/* ML_1 (gtk_source_view_get_show_line_numbers, GtkSourceView_val, Val_bool) */ -/* ML_2 (gtk_source_view_set_show_line_numbers, GtkSourceView_val, Bool_val, Unit) */ +ML_0 (gtk_source_languages_manager_new, Val_GtkAny_sink) +ML_2 (gtk_source_languages_manager_get_language_from_mime_type, + GtkSourceLanguagesManager_val, String_val, Val_GtkAny) +/* ML_0 (gtk_source_buffer_new, GtkSourceTagTable_val, Val_GtkAny_sink) */ +/* ML_1 (gtk_source_buffer_new_with_language, GtkSourceLanguage_val, + Val_GtkAny_sink) */ ML_1 (gtk_source_buffer_can_undo, GtkSourceBuffer_val, Bool_val) ML_1 (gtk_source_buffer_can_redo, GtkSourceBuffer_val, Bool_val) ML_1 (gtk_source_buffer_undo, GtkSourceBuffer_val, Unit) @@ -92,3 +97,6 @@ ML_1 (gtk_source_buffer_redo, GtkSourceBuffer_val, Unit) ML_1 (gtk_source_buffer_begin_not_undoable_action, GtkSourceBuffer_val, Unit) ML_1 (gtk_source_buffer_end_not_undoable_action, GtkSourceBuffer_val, Unit) +ML_0 (gtk_source_view_new, Val_GtkWidget_sink) +ML_1 (gtk_source_view_new_with_buffer, GtkSourceBuffer_val, Val_GtkWidget_sink) + diff --git a/helm/DEVEL/lablgtksourceview/test/test.ml b/helm/DEVEL/lablgtksourceview/test/test.ml index 6eb369dfb..02a0806e2 100644 --- a/helm/DEVEL/lablgtksourceview/test/test.ml +++ b/helm/DEVEL/lablgtksourceview/test/test.ml @@ -27,17 +27,8 @@ open Printf let win = GWindow.window ~title:"LablGtkSourceView test" () let scrolled_win = GBin.scrolled_window ~packing:win#add () -let text = - let ic = open_in "test.txt" in - let size = in_channel_length ic in - let buf = String.create size in - really_input ic buf 0 size; - close_in ic; - buf -let source_buffer = GSourceView.source_buffer ~text ~check_brackets:true () let source_view = GSourceView.source_view - ~source_buffer ~auto_indent:true ~insert_spaces_instead_of_tabs:true ~tabs_width:2 ~show_line_numbers:true ~margin:80 ~show_margin:true @@ -45,7 +36,16 @@ let source_view = ~packing:scrolled_win#add ~height:500 ~width:650 () let _ = + let text = + let ic = open_in "test.txt" in + let size = in_channel_length ic in + let buf = String.create size in + really_input ic buf 0 size; + close_in ic; + buf + in win#set_allow_shrink true; + source_view#source_buffer#set_text text; ignore (win#connect#destroy (fun _ -> GMain.quit ())); (* ignore (source_view#connect#move_cursor (fun _ _ ~extend -> prerr_endline "move_cursor"));