]> matita.cs.unibo.it Git - helm.git/commitdiff
snapshot
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 9 Jun 2005 15:34:11 +0000 (15:34 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 9 Jun 2005 15:34:11 +0000 (15:34 +0000)
- almost fully bound SourceView
- started binding of SourceBuffer

helm/DEVEL/lablgtksourceview/gSourceView.ml
helm/DEVEL/lablgtksourceview/gSourceView.mli
helm/DEVEL/lablgtksourceview/gtkSourceView.ml
helm/DEVEL/lablgtksourceview/gtkSourceView.props
helm/DEVEL/lablgtksourceview/gtk_sourceview.ml
helm/DEVEL/lablgtksourceview/test/test.ml

index 9a4534f833f9ab8a1363254e2acf1ab89b4432fe..372493c815978b8fb79d3996ae9829cd9840d942 100644 (file)
@@ -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 =
index 4b1b60be691a96e0437a7b20167f8b1312047206..eb024bfcbcc68f6eecc3c7f10a01c63782e8ee9e 100644 (file)
@@ -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 :
index ff66d0278a5e3b03c3985862d6bf2cdec345c5af..87ae6b02505fb74f86859353e04c7bb89175223a 100644 (file)
@@ -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
+
index b506fe9d449e8767936bbf71c18a75ef0178e2f0..1ff069b43f31ad2e6ea1d38e8b1b4b14ba65659f 100644 (file)
@@ -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
+}
+
index e6a513f1234f3201bdea70365b8f97f785f11238..8c1f6be6c5c915e4540f540e7ca4552a3ecc6a7f 100644 (file)
@@ -24,4 +24,5 @@
  *)
 
 type source_view = [Gtk.text_view|`sourceview]
+type source_buffer = [Gtk.text_buffer|`sourcebuffer]
 
index e0662a0f8520ee26e6d676500e67e72ed43d09b6..4979ad02d486f144c122b7c87e3425fa2078b8ee 100644 (file)
@@ -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 ()