From: Stefano Zacchiroli Date: Thu, 9 Jun 2005 20:48:04 +0000 (+0000) Subject: snapshot X-Git-Tag: PRE_STORAGE~92 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=74d02fcdf866ef4d156e56cc890ee4ce2637f5d9;p=helm.git snapshot - implemented many methods of GtkSourceBuffer - fixed creation of GtkSourceView (no longer assert failure on undo) --- diff --git a/helm/DEVEL/lablgtksourceview/Makefile.in b/helm/DEVEL/lablgtksourceview/Makefile.in index ebd0adc46..0082f6e39 100644 --- a/helm/DEVEL/lablgtksourceview/Makefile.in +++ b/helm/DEVEL/lablgtksourceview/Makefile.in @@ -33,16 +33,19 @@ OCAML_STUB_DIR = @OCAML_STUB_DIR@ ARCHIVE = $(PACKAGE) DLL = dll$(ARCHIVE).so -TESTDIR = ./test -TMPDIR = .test -TMPPKGDIR = $(TMPDIR)/$(PACKAGE) - -all: $(ARCHIVE).cma -opt: $(ARCHIVE).cmxa -test: $(TESTDIR)/test -test.opt: $(TESTDIR)/test.opt +TESTDIR = test + +all: $(ARCHIVE).cma $(TESTDIR)/test +opt: $(ARCHIVE).cmxa $(TESTDIR)/test.opt + world: all opt +.PHONY: test/test test/test.opt +test/test.opt: + $(MAKE) -C $(TESTDIR) test.opt +test/test: + $(MAKE) -C $(TESTDIR) test + dist: rm -rf $(DIST_DIR)/ mkdir $(DIST_DIR)/ @@ -84,18 +87,6 @@ $(ARCHIVE).cma $(DLL): $(OBJECTS) $(OBJECTS_C) $(ARCHIVE).cmxa $(ARCHIVE).a: $(OBJECTS_OPT) $(OCAMLMKLIB) -o $(ARCHIVE) -L$(OCAML_STUB_DIR) $^ $(OBJECTS_C) $(SHARED_LIBS) -$(TESTDIR)/test: $(OBJECTS_C) $(ARCHIVE).cma $(TESTDIR)/test.ml - mkdir -p $(TMPPKGDIR) - cp $(OBJECTS_C) $(DLL) $(ARCHIVE).cma $(INST) $(TMPPKGDIR) - cd $(TESTDIR) ; export OCAMLPATH=../$(TMPDIR):$$OCAMLPATH ; make - rm -r $(TMPDIR) - -$(TESTDIR)/test.opt: $(OBJECTS_C) $(ARCHIVE).a $(ARCHIVE).cmxa $(TESTDIR)/test.ml - mkdir -p $(TMPPKGDIR) - cp $(OBJECTS_C) $(ARCHIVE).a $(ARCHIVE).cmxa $(INST) $(TMPPKGDIR) - cd $(TESTDIR) ; export OCAMLPATH=../$(TMPDIR):$$OCAMLPATH ; make opt - rm -r $(TMPDIR) - install: test ! -f $(ARCHIVE).cmxa || extra="$(ARCHIVE).a $(ARCHIVE).cmxa" ; \ if [ "$(PREFIX)" = "" ]; then \ @@ -117,8 +108,7 @@ uninstall: clean: rm -f *.[ao] *.cm[iaxo] *.cmxa *.so $(GENERATED_FILES) - cd $(TESTDIR) ; make clean - rm -rf $(TMPDIR) + make -C $(TESTDIR) clean distclean: clean rm -f config.log config.cache config.status Makefile META diff --git a/helm/DEVEL/lablgtksourceview/gSourceView.ml b/helm/DEVEL/lablgtksourceview/gSourceView.ml index 372493c81..ec449377b 100644 --- a/helm/DEVEL/lablgtksourceview/gSourceView.ml +++ b/helm/DEVEL/lablgtksourceview/gSourceView.ml @@ -36,11 +36,55 @@ 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 -class source_view_signals obj_param = +(** {2 GtkSourceBuffer} *) + +class source_buffer_signals obj_arg = +object + inherit ['a] gobject_signals (obj_arg : [> Gtk_sourceview.source_buffer] obj) + inherit GText.buffer_signals obj_arg + inherit source_buffer_sigs +end + +class source_buffer (obj: Gtk_sourceview.source_buffer obj) = +object (self) + inherit GText.buffer_skel obj + method connect = new source_buffer_signals obj + method misc = new gobject_ops obj + method check_brackets = get_bool (self#misc#get_property "check-brackets") + method set_check_brackets x = self#misc#set_property "check-brackets" (bool x) + method highlight = get_bool (self#misc#get_property "highlight") + method set_highlight x = self#misc#set_property "highlight" (bool x) + 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 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 + method can_redo = SourceBuffer.can_redo obj + method undo () = SourceBuffer.undo obj + method redo () = SourceBuffer.redo obj + method begin_not_undoable_action () = + SourceBuffer.begin_not_undoable_action obj + method end_not_undoable_action () = + SourceBuffer.end_not_undoable_action obj +end + +let source_buffer = + SourceBuffer.make_params [] ~cont:(fun pl () -> + new source_buffer (SourceBuffer.create pl)) + + (* alias used below, needed because "source_buffer" is a name in scope *) +let source_buffer' = source_buffer + +(** {2 GtkSourceView} *) + +class source_view_signals obj_arg = object - inherit widget_signals_impl (obj_param : [> Gtk_sourceview.source_view] obj) - inherit GText.view_signals obj_param + inherit widget_signals_impl (obj_arg : [> Gtk_sourceview.source_view] obj) + inherit GText.view_signals obj_arg inherit source_view_sigs end @@ -72,9 +116,16 @@ object (self) method smart_home_end = get_bool (self#misc#get_property "smart_home_end") end -let source_view = +let source_view ?source_buffer = SourceView.make_params [] ~cont:( GtkText.View.make_params ~cont:( GContainer.pack_container ~create:(fun pl -> - new source_view (SourceView.create pl)))) + let buf = + match source_buffer with + | None -> source_buffer' () + | Some source_buffer -> source_buffer + in + let obj = SourceView.create pl in + GtkText.View.set_buffer obj buf#as_buffer; + new source_view obj))) diff --git a/helm/DEVEL/lablgtksourceview/gSourceView.mli b/helm/DEVEL/lablgtksourceview/gSourceView.mli index eb024bfcb..e7bc27638 100644 --- a/helm/DEVEL/lablgtksourceview/gSourceView.mli +++ b/helm/DEVEL/lablgtksourceview/gSourceView.mli @@ -25,6 +25,90 @@ open Gtk +(** {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 : + 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 + end + +class source_buffer: + Gtk_sourceview.source_buffer Gtk.obj -> + object + inherit GText.buffer_skel + method connect: source_buffer_signals + method misc: GObj.gobject_ops + method check_brackets: bool + method set_check_brackets: bool -> unit +(* method set_bracket_match_style: tag_style -> unit *) + method highlight: bool + 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 escape_char: Glib.unichar + method set_escape_char: Glib.unichar -> unit + method can_undo: bool + method can_redo: bool + method undo: unit -> unit + method redo: unit -> unit + method begin_not_undoable_action: unit -> unit + method end_not_undoable_action: unit -> unit +(* method create_marker: name:char -> typ:char -> source_marker *) +(* method move_marker: source_marker -> Gtext.text_iter -> unit *) +(* method delete_marker: source_marker -> unit *) +(* method get_marker: name:char -> source_marker *) +(* method get_markers_in_region: + start:text_iter -> stop:text_iter -> source_marker list *) +(* method get_first_marker: unit -> source_marker *) +(* method get_last_marker: unit -> source_marker *) +(* method get_iter_at_marker: ... *) +(* method get_next_marker: unit -> source_marker *) +(* method get_prev_marker: unit -> source_marker *) + end + +val source_buffer : + ?check_brackets:bool -> + ?escape_char:int -> + ?highlight:bool -> + ?max_undo_levels:int -> +(* ?tag_table:GText.tag_table -> + ?text:string -> *) + unit -> + source_buffer + +(** {2 GtkSourceView} *) + class source_view_signals : ([> Gtk_sourceview.source_view ] as 'b) obj -> object ('a) @@ -80,6 +164,7 @@ class source_view : end val source_view : + ?source_buffer:source_buffer -> ?auto_indent:bool -> ?insert_spaces_instead_of_tabs:bool -> ?margin:int -> diff --git a/helm/DEVEL/lablgtksourceview/gtkSourceView.ml b/helm/DEVEL/lablgtksourceview/gtkSourceView.ml index 87ae6b025..87745712e 100644 --- a/helm/DEVEL/lablgtksourceview/gtkSourceView.ml +++ b/helm/DEVEL/lablgtksourceview/gtkSourceView.ml @@ -31,8 +31,12 @@ open Tags open GtkSourceViewProps open GtkBase -external _gtksourceview_init : unit -> unit = "ml_gtk_sourceview_init" -let () = _gtksourceview_init () +external _gtk_source_view_init : unit -> unit = "ml_gtk_source_view_init" +external _gtk_source_buffer_init : unit -> unit = "ml_gtk_source_buffer_init" + +let () = + _gtk_source_view_init (); + _gtk_source_buffer_init () module SourceView = struct @@ -42,5 +46,15 @@ end module SourceBuffer = struct include SourceBuffer + external can_undo: [>`sourcebuffer] obj -> bool = + "ml_gtk_source_buffer_can_undo" + external can_redo: [>`sourcebuffer] obj -> bool = + "ml_gtk_source_buffer_can_redo" + external undo: [>`sourcebuffer] obj -> unit = "ml_gtk_source_buffer_undo" + external redo: [>`sourcebuffer] obj -> unit = "ml_gtk_source_buffer_redo" + external begin_not_undoable_action: [>`sourcebuffer] obj -> unit = + "ml_gtk_source_buffer_begin_not_undoable_action" + external end_not_undoable_action: [>`sourcebuffer] obj -> unit = + "ml_gtk_source_buffer_end_not_undoable_action" end diff --git a/helm/DEVEL/lablgtksourceview/gtkSourceView.props b/helm/DEVEL/lablgtksourceview/gtkSourceView.props index 1ff069b43..25885c796 100644 --- a/helm/DEVEL/lablgtksourceview/gtkSourceView.props +++ b/helm/DEVEL/lablgtksourceview/gtkSourceView.props @@ -24,5 +24,9 @@ class SourceBuffer type "source_buffer obj" set wrapsig : GObject { "highlight" gboolean : Read / Write "language" GtkSourceLanguage : Read / Write "max-undo-levels" gint : Read / Write + signal can_redo: gboolean + signal can_undo: gboolean + signal highlight_updated: GtkTextIter GtkTextIter + signal marker_updated: GtkTextIter } diff --git a/helm/DEVEL/lablgtksourceview/ml_gtk_sourceview.c b/helm/DEVEL/lablgtksourceview/ml_gtk_sourceview.c index 935e96ac3..eb0a69dc5 100644 --- a/helm/DEVEL/lablgtksourceview/ml_gtk_sourceview.c +++ b/helm/DEVEL/lablgtksourceview/ml_gtk_sourceview.c @@ -47,14 +47,20 @@ /* Init all */ -CAMLprim value ml_gtk_sourceview_init(value unit) -{ - /* Since these are declared const, must force gcc to call them! */ +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); } +CAMLprim value ml_gtk_source_buffer_init(value unit) +{ /* Since these are declared const, must force gcc to call them! */ + GType t = gtk_source_buffer_get_type(); + return Val_GType(t); +} + #define GtkSourceView_val(val) check_cast(GTK_SOURCE_VIEW,val) +#define GtkSourceBuffer_val(val) check_cast(GTK_SOURCE_BUFFER,val) //##################################### // @@ -76,8 +82,13 @@ value ml_##cname (value arg1, value arg2, value arg3) { return Val_option_ptr((c 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_view_get_show_line_numbers, GtkSourceView_val, - Val_bool) -ML_2 (gtk_source_view_set_show_line_numbers, GtkSourceView_val, - Bool_val, Unit) +/* 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_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) +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) diff --git a/helm/DEVEL/lablgtksourceview/test/Makefile.in b/helm/DEVEL/lablgtksourceview/test/Makefile.in index 007c17815..d4c5864bc 100644 --- a/helm/DEVEL/lablgtksourceview/test/Makefile.in +++ b/helm/DEVEL/lablgtksourceview/test/Makefile.in @@ -9,10 +9,10 @@ TMPDIR = .test all: test opt: test.opt -test: test.ml +test: test.ml ../$(PACKAGE).cma $(OCAMLC) $(LINKFLAGS) $(PACKAGE).cma -o $@ $< -test.opt: test.ml +test.opt: test.ml ../$(PACKAGE).cmxa $(OCAMLOPT) $(LINKFLAGS) $(PACKAGE).cmxa -o $@ $< clean: diff --git a/helm/DEVEL/lablgtksourceview/test/test.ml b/helm/DEVEL/lablgtksourceview/test/test.ml index 4979ad02d..08c942bc5 100644 --- a/helm/DEVEL/lablgtksourceview/test/test.ml +++ b/helm/DEVEL/lablgtksourceview/test/test.ml @@ -27,21 +27,21 @@ open Printf let win = GWindow.window ~title:"LablGtkSourceView test" () let vbox = GPack.vbox ~packing:win#add () +let source_buffer = GSourceView.source_buffer ~check_brackets:true () let source_view = - GSourceView.source_view ~packing:vbox#add ~height:400 ~width:300 + GSourceView.source_view + ~source_buffer + ~auto_indent:true ~insert_spaces_instead_of_tabs:true ~tabs_width:2 ~show_line_numbers:true + ~margin:30 ~show_margin:true + ~smart_home_end:true + ~packing:vbox#add ~height:400 ~width:300 () let _ = ignore (win#connect#destroy (fun _ -> GMain.quit ())); 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 ()