aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-07 18:55:28 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-07 18:55:28 +0000
commit9ea3d852e24873a4b5eb4d2cc3d348e7ddcbb48a (patch)
tree45edacf9b7013d026d0de6eb83fc2ea3b4522e6d
parenteda60e3598ae499120913c37ccf8295e2a75d29d (diff)
Coqide: cleanup concerning insert_text signal
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16044 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--ide/coqide.ml66
1 files changed, 41 insertions, 25 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 9dfbf2f2e..3c741d4a0 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -10,6 +10,37 @@ open Preferences
open Gtk_parsing
open Ideutils
+(** Note concerning GtkTextBuffer
+
+ Be careful with gtk calls on text buffers, since many are non-atomic :
+ they emit a gtk signal and the handlers for this signal are run
+ immediately, before returning to the current function.
+ Here's a partial list of these signals and the methods that
+ trigger them (cf. documentation of GtkTextBuffer, signal section)
+
+ begin_user_action : #begin_user_action, #insert_interactive,
+ #insert_range_interactive, #delete_interactive, #delete_selection
+ end_user_action : #end_user_action, #insert_interactive,
+ #insert_range_interactive, #delete_interactive, #delete_selection
+
+ insert_text : #insert (and variants)
+ delete_range : #delete (and variants)
+
+ apply_tag : #apply_tag, (and some #insert)
+ remove_tag : #remove_tag
+
+ mark_deleted : #delete_mark
+ mark_set : #create_mark, #move_mark
+
+ changed : ... (whenever a buffer has changed)
+ modified_changed : #set_modified (and whenever the modified bit flips)
+
+ Caveat : when the buffer is modified, all iterators on it become
+ invalid and shouldn't be used (nasty errors otherwise). There are
+ some special cases : boundaries given to #insert and #delete are
+ revalidated by the default signal handler.
+*)
+
type direction = Up | Down
type flag = [ `COMMENT | `UNSAFE ]
@@ -884,26 +915,18 @@ object(self)
initializer
ignore (input_buffer#connect#insert_text
~callback:(fun it s ->
+ (* If a #insert happens in the locked zone, we discard it.
+ Other solution: always use #insert_interactive and similar *)
if (it#compare self#get_start_of_input)<0
then GtkSignal.stop_emit ();
- if String.length s > 1 then
- (Minilib.log "insert_text: Placing cursor";input_buffer#place_cursor ~where:it)));
- ignore (input_buffer#connect#after#apply_tag
- ~callback:(fun tag ~start ~stop ->
- if (start#compare self#get_start_of_input)>=0
- then
- begin
- input_buffer#remove_tag
- Tags.Script.processed
- ~start
- ~stop;
- input_buffer#remove_tag
- Tags.Script.unjustified
- ~start
- ~stop
- end
- )
- );
+ if String.length s > 1 then begin
+ Minilib.log "insert_text: Placing cursor";
+ input_buffer#place_cursor ~where:it
+ end;
+ if String.contains s '\n' then begin
+ Minilib.log "insert_text: Recentering";
+ self#recenter_insert
+ end));
ignore (input_buffer#connect#begin_user_action
~callback:(fun () ->
let where = self#get_insert in
@@ -931,13 +954,6 @@ object(self)
Minilib.log (s^" moved")
| None -> () )
);
- ignore (input_buffer#connect#insert_text
- ~callback:(fun it s ->
- Minilib.log "Should recenter ?";
- if String.contains s '\n' then begin
- Minilib.log "Should recenter: yes";
- self#recenter_insert
- end));
Coq.grab mycoqtop self#include_file_dir_in_path;
end