From c96fc8dc30d68077eb5b2ef079dd7d5afeb56132 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Wed, 16 May 2012 16:02:14 +0000 Subject: Trying to fix bug #2780, by short-circuiting the Gtk signals. A bit hackish. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15334 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/wg_ScriptView.ml | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) (limited to 'ide/wg_ScriptView.ml') diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 8c679e4c1..cf0667f7b 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -226,6 +226,33 @@ object (self) (* HACK: Redirect the undo/redo signals of the underlying GtkSourceView *) ignore (self#connect#undo (fun _ -> ignore (self#undo ()); GtkSignal.stop_emit())); ignore (self#connect#redo (fun _ -> ignore (self#redo ()); GtkSignal.stop_emit())); + (* HACK: Redirect the move_line signal of the underlying GtkSourceView *) + let move_line_marshal = GtkSignal.marshal2 + Gobject.Data.boolean Gobject.Data.int "move_line_marshal" + in + let move_line_signal = { + GtkSignal.name = "move-lines"; + classe = Obj.magic 0; + marshaller = move_line_marshal; } + in + let callback b i = + let rec start_line iter = + if iter#starts_line then iter + else start_line iter#backward_char + in + let iter = start_line (self#buffer#get_iter `INSERT) in + (* do we forward the signal? *) + let proceed = + if not b && i = 1 then + iter#editable true && iter#forward_line#editable true + else if not b && i = -1 then + iter#editable true && iter#backward_line#editable true + else false + in + if not proceed then GtkSignal.stop_emit () + in + ignore(GtkSignal.connect ~sgn:move_line_signal ~callback obj); + () end -- cgit v1.2.3