From: Stefano Zacchiroli Date: Thu, 9 Jun 2005 15:34:11 +0000 (+0000) Subject: snapshot X-Git-Tag: PRE_INDEX_1~9 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c270254a72b6079e4468aa52d9dcad8528058506;p=helm.git snapshot - almost fully bound SourceView - started binding of SourceBuffer --- diff --git a/helm/DEVEL/lablgtksourceview/gSourceView.ml b/helm/DEVEL/lablgtksourceview/gSourceView.ml index 9a4534f83..372493c81 100644 --- a/helm/DEVEL/lablgtksourceview/gSourceView.ml +++ b/helm/DEVEL/lablgtksourceview/gSourceView.ml @@ -32,14 +32,14 @@ open GtkSourceView open OgtkSourceViewProps open GObj -let get_bool = function - | `BOOL b -> b - | _ -> assert false +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 class source_view_signals obj_param = object inherit widget_signals_impl (obj_param : [> Gtk_sourceview.source_view] obj) -(* inherit OgtkTextProps.text_view_sigs *) inherit GText.view_signals obj_param inherit source_view_sigs end @@ -48,10 +48,28 @@ class source_view (obj: Gtk_sourceview.source_view obj) = object (self) inherit GText.view_skel obj 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 = get_bool (self#misc#get_property "show_line_numbers") - method set_show_line_numbers b = - self#misc#set_property "show_line_numbers" (`BOOL b) + method set_show_line_markers x = + self#misc#set_property "show_line_markers" (bool x) + method show_line_markers = + get_bool (self#misc#get_property "show_line_markers") + method set_tabs_width x = self#misc#set_property "tabs_width" (uint x) + method tabs_width = get_uint (self#misc#get_property "tabs_width") + method set_auto_indent x = self#misc#set_property "auto_indent" (bool x) + method auto_indent = get_bool (self#misc#get_property "auto_indent") + method set_insert_spaces_instead_of_tabs x = + self#misc#set_property "insert_spaces_instead_of_tabs" (bool x) + method insert_spaces_instead_of_tabs = + get_bool (self#misc#get_property "insert_spaces_instead_of_tabs") + method set_show_margin x = self#misc#set_property "show_margin" (bool x) + method show_margin = get_bool (self#misc#get_property "show_margin") + method set_margin x = self#misc#set_property "margin" (uint x) + method margin = get_uint (self#misc#get_property "margin") + method set_smart_home_end x = self#misc#set_property "smart_home_end" (bool x) + method smart_home_end = get_bool (self#misc#get_property "smart_home_end") end let source_view = diff --git a/helm/DEVEL/lablgtksourceview/gSourceView.mli b/helm/DEVEL/lablgtksourceview/gSourceView.mli index 4b1b60be6..eb024bfcb 100644 --- a/helm/DEVEL/lablgtksourceview/gSourceView.mli +++ b/helm/DEVEL/lablgtksourceview/gSourceView.mli @@ -56,74 +56,27 @@ class source_view_signals : class source_view : Gtk_sourceview.source_view Gtk.obj -> object - method add_child_at_anchor : GObj.widget -> GText.child_anchor -> unit - method add_child_in_window : - child:GObj.widget -> - which_window:Gtk.Tags.text_window_type -> x:int -> y:int -> unit - method as_view : Gtk.text_view Gtk.obj - method as_widget : Gtk.widget Gtk.obj - method backward_display_line : GText.iter -> bool - method backward_display_line_start : GText.iter -> bool - method buffer : GText.buffer - method buffer_to_window_coords : - tag:Gtk.Tags.text_window_type -> x:int -> y:int -> int * int - method coerce : GObj.widget - method connect : source_view_signals - method cursor_visible : bool - method destroy : unit -> unit - method drag : GObj.drag_ops - method editable : bool - method event : GObj.event_ops - method forward_display_line : GText.iter -> bool - method forward_display_line_end : GText.iter -> bool - method get_border_window_size : - [ `BOTTOM | `LEFT | `RIGHT | `TOP ] -> int - method get_iter_at_location : x:int -> y:int -> GText.iter - method get_iter_location : GText.iter -> Gdk.Rectangle.t - method get_line_at_y : int -> GText.iter * int - method get_line_yrange : GText.iter -> int * int - method get_oid : int - method get_window : Gtk.Tags.text_window_type -> Gdk.window option - method get_window_type : Gdk.window -> Gtk.Tags.text_window_type - method indent : int - method justification : Gtk.Tags.justification - method left_margin : int - method misc : GObj.misc_ops - method move_child : child:GObj.widget -> x:int -> y:int -> unit - method move_mark_onscreen : GText.mark -> bool - method move_visually : GText.iter -> int -> bool - method pixels_above_lines : int - method pixels_below_lines : int - method pixels_inside_wrap : int - method place_cursor_onscreen : unit -> bool - method right_margin : int - method scroll_mark_onscreen : GText.mark -> unit - method scroll_to_iter : - ?within_margin:float -> - ?use_align:bool -> ?xalign:float -> ?yalign:float -> GText.iter -> bool - method scroll_to_mark : - ?within_margin:float -> - ?use_align:bool -> ?xalign:float -> ?yalign:float -> GText.mark -> unit - method set_border_window_size : - typ:[ `BOTTOM | `LEFT | `RIGHT | `TOP ] -> size:int -> unit - method set_buffer : GText.buffer -> unit - method set_cursor_visible : bool -> unit - method set_editable : bool -> unit - method set_indent : int -> unit - method set_justification : Gtk.Tags.justification -> unit - method set_left_margin : int -> unit - method set_pixels_above_lines : int -> unit - method set_pixels_below_lines : int -> unit - method set_pixels_inside_wrap : int -> unit - method set_right_margin : int -> unit + inherit GText.view_skel + val obj: Gtk_sourceview.source_view Gtk.obj + method connect: source_view_signals method set_show_line_numbers : bool -> unit - method set_wrap_mode : Gtk.Tags.wrap_mode -> unit method show_line_numbers : bool - method starts_display_line : GText.iter -> bool - method visible_rect : Gdk.Rectangle.t - method window_to_buffer_coords : - tag:Gtk.Tags.text_window_type -> x:int -> y:int -> int * int - method wrap_mode : Gtk.Tags.wrap_mode + 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 + method auto_indent: bool + method set_insert_spaces_instead_of_tabs: bool -> unit + method insert_spaces_instead_of_tabs: bool + method set_show_margin: bool -> unit + method show_margin: bool + method set_margin: int -> unit + method margin: int +(* method set_marker_pixbuf: GdkPixbuf.pixbuf -> unit *) +(* method marker_pixbuf: GdkPixbuf.pixbuf *) + method set_smart_home_end: bool -> unit + method smart_home_end: bool end val source_view : diff --git a/helm/DEVEL/lablgtksourceview/gtkSourceView.ml b/helm/DEVEL/lablgtksourceview/gtkSourceView.ml index ff66d0278..87ae6b025 100644 --- a/helm/DEVEL/lablgtksourceview/gtkSourceView.ml +++ b/helm/DEVEL/lablgtksourceview/gtkSourceView.ml @@ -34,7 +34,13 @@ open GtkBase external _gtksourceview_init : unit -> unit = "ml_gtk_sourceview_init" let () = _gtksourceview_init () -module SourceView = struct +module SourceView = +struct include SourceView end +module SourceBuffer = +struct + include SourceBuffer +end + diff --git a/helm/DEVEL/lablgtksourceview/gtkSourceView.props b/helm/DEVEL/lablgtksourceview/gtkSourceView.props index b506fe9d4..1ff069b43 100644 --- a/helm/DEVEL/lablgtksourceview/gtkSourceView.props +++ b/helm/DEVEL/lablgtksourceview/gtkSourceView.props @@ -7,7 +7,7 @@ header { class SourceView type "source_view obj" set wrapsig : Widget { "auto-indent" gboolean : Read / Write - "insert-spaces-instead-of-tabs" 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 @@ -18,3 +18,11 @@ class SourceView type "source_view obj" set wrapsig : Widget { signal undo } +class SourceBuffer type "source_buffer obj" set wrapsig : GObject { + "check-brackets" gboolean : Read / Write + "escape-char" guint : Read / Write + "highlight" gboolean : Read / Write + "language" GtkSourceLanguage : Read / Write + "max-undo-levels" gint : Read / Write +} + diff --git a/helm/DEVEL/lablgtksourceview/gtk_sourceview.ml b/helm/DEVEL/lablgtksourceview/gtk_sourceview.ml index e6a513f12..8c1f6be6c 100644 --- a/helm/DEVEL/lablgtksourceview/gtk_sourceview.ml +++ b/helm/DEVEL/lablgtksourceview/gtk_sourceview.ml @@ -24,4 +24,5 @@ *) type source_view = [Gtk.text_view|`sourceview] +type source_buffer = [Gtk.text_buffer|`sourcebuffer] diff --git a/helm/DEVEL/lablgtksourceview/test/test.ml b/helm/DEVEL/lablgtksourceview/test/test.ml index e0662a0f8..4979ad02d 100644 --- a/helm/DEVEL/lablgtksourceview/test/test.ml +++ b/helm/DEVEL/lablgtksourceview/test/test.ml @@ -36,6 +36,12 @@ let _ = ignore (source_view#connect#move_cursor (fun _ _ ~extend -> prerr_endline "move_cursor")); ignore (source_view#connect#undo (fun _ -> prerr_endline "undo")); + source_view#set_auto_indent true; + source_view#set_insert_spaces_instead_of_tabs true; + source_view#set_tabs_width 2; + source_view#set_margin 30; + source_view#set_show_margin true; + source_view#set_smart_home_end true; win#show (); GMain.Main.main ()