implement support for drgeocaml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7575 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 22 insertions, 3 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 48bb19cb6f..d9f02d8402 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -3364,6 +3364,24 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 
 ;;
 
+(* This function check every half of second if DrGeoCaml has send 
+   something on his private clipboard *)
+
+let rec check_for_drgeocaml_input () = 
+  let cb_Dr = GData.clipboard (Gdk.Atom.intern "_DrGeoCaml") in
+    while true do
+      Thread.delay 0.5;
+      let s = cb_Dr#text in
+	(match s with 
+	     Some s -> 
+	       (get_current_view()).view#buffer#insert (s^"\n")
+	   | None -> ()
+	);
+	(* cb_Dr#clear does not work so i use : *)
+	cb_Dr#set_text "" 
+    done
+
+
 let start () = 
   let files = Coq.init () in
   ignore_break ();
@@ -3382,9 +3400,10 @@ let start () =
   Command_windows.main ();
   Blaster_window.main 9;
   main files;
+  ignore (Thread.create check_for_drgeocaml_input ()); 
   while true do 
     try 
-      GtkThread.main ()
+      GtkThread.main ()	
     with
       | Sys.Break -> prerr_endline "Interrupted." ; flush stderr
       | e -> 
diff --git a/ide/undo.ml b/ide/undo.ml
index 0b4ea17260..7a62cd558b 100644
--- a/ide/undo.ml
+++ b/ide/undo.ml
@@ -18,7 +18,7 @@ let neg act = match act with
   | Insert (s,i,l) -> Delete (s,i,l)
   | Delete (s,i,l) -> Insert (s,i,l)
 
-class undoable_view (tv:Gtk.text_view Gtk.obj) =
+class undoable_view (tv:([> Gtk.text_view ] as 'a) Gtk.obj) =
   let undo_lock = ref true in 
 object(self)
   inherit GText.view tv as super
diff --git a/ide/undo.mli b/ide/undo.mli
index 82bcf2384d..1ea8fbea09 100644
--- a/ide/undo.mli
+++ b/ide/undo.mli
@@ -10,7 +10,7 @@
 
 (* An undoable view class *)
 
-class undoable_view : Gtk.text_view Gtk.obj ->
+class undoable_view : [>Gtk.text_view] Gtk.obj ->
 object
   inherit GText.view
   method undo : bool