diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-16 16:02:14 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-16 16:02:14 +0000 |
commit | c96fc8dc30d68077eb5b2ef079dd7d5afeb56132 (patch) | |
tree | 4c8e7a0e15ab1d79e43f3e5259cad7c1c880faaa | |
parent | b2fcd2f27295f0fbb24c9ee95b1ebdfc712bcd83 (diff) |
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
-rw-r--r-- | ide/wg_ScriptView.ml | 27 |
1 files changed, 27 insertions, 0 deletions
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 |