Coqide Detach View: avoid doing gtk stuff in sub-thread (fix #2863)

 In Win32, playing with gtk stuff outside gtk's main loop causes
 coqide to crash: we should be careful when using do_if_not_computing
 and its Thread.create. In the case of Detach View anyway, the
 do_if_not_computing was clearly useless. Strangely, the unix gtk
 seems more resilient and was not crashing ...

 Btw, avoid maintaining a thread-unsafe list of detached_views,
 use instead gtk callbacks to close detached views when their
 corresponding buffer in the main window is closed.

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

1 files changed, 27 insertions, 41 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 75a5c5ae3..0fac50abe 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -21,10 +21,6 @@ type ide_info = {
 class type _analyzed_view =
 object
 
-  method kill_detached_views : unit -> unit
-  method add_detached_view : GWindow.window -> unit
-  method remove_detached_view : GWindow.window -> unit
-
   method filename : string option
   method stats :  Unix.stats option
   method update_stats : unit
@@ -64,7 +60,10 @@ type viewable_script = {
 }
 
 let kill_session s =
-  s.analyzed_view#kill_detached_views ();
+  (* To close the detached views of this script, we call manually
+     [destroy] on it, triggering some callbacks in [detach_view].
+     In a more modern lablgtk, rather use the page-removed signal ? *)
+  s.script#destroy ();
   Coq.close_coqtop s.toplvl
 
 let build_session s =
@@ -437,19 +436,9 @@ object(self)
   val mutable stats = None
   val mutable last_modification_time = 0.
   val mutable last_auto_save_time = 0.
-  val mutable detached_views = []
 
   val hidden_proofs = Hashtbl.create 32
 
-  method add_detached_view (w:GWindow.window) =
-    detached_views <- w::detached_views
-  method remove_detached_view (w:GWindow.window) =
-    detached_views <- List.filter (fun e -> w#misc#get_oid<>e#misc#get_oid) detached_views
-
-  method kill_detached_views () =
-    List.iter (fun w -> w#destroy ()) detached_views;
-    detached_views <- []
-
   method filename = filename
   method stats = stats
   method update_stats =
@@ -1791,6 +1780,28 @@ let main files =
 	|Some ac -> GAction.add_action name ~label ~callback ~accel:(current.modifier_for_templates^ac)
 	|None -> GAction.add_action name ~label ~callback ?accel:None
   in
+  let detach_view _ =
+    (* Open a separate window containing the current buffer *)
+    let trm = session_notebook#current_term in
+    let file = match trm.analyzed_view#filename with
+      | None -> "*scratch*"
+      | Some f -> f
+    in
+    let w = GWindow.window ~show:true
+      ~width:(current.window_width*2/3)
+      ~height:(current.window_height*2/3)
+      ~position:`CENTER
+      ~title:file
+      ()
+    in
+    let sb = GBin.scrolled_window ~packing:w#add ()
+    in
+    let nv = GText.view ~buffer:trm.script#buffer ~packing:sb#add ()
+    in
+    nv#misc#modify_font current.text_font;
+    (* If the buffer in the main window is closed, destroy this detached view *)
+    ignore (trm.script#connect#destroy ~callback:w#destroy)
+  in
     GAction.add_actions file_actions [
       GAction.add_action "File" ~label:"_File";
       GAction.add_action "New" ~callback:new_f ~stock:`NEW;
@@ -1988,32 +1999,7 @@ let main files =
     GAction.add_actions windows_actions [
       GAction.add_action "Windows" ~label:"_Windows";
       GAction.add_action "Detach View" ~label:"Detach _View"
-	~callback:(fun _ -> let p = session_notebook#current_term in
-                     do_if_not_computing p "detach view"
-		     (function handle ->
-			let w = GWindow.window ~show:true
-			  ~width:(current.window_width*2/3)
-			  ~height:(current.window_height*2/3)
-			  ~position:`CENTER
-			  ~title:(match p.analyzed_view#filename with
-				    | None -> "*Unnamed*"
-				    | Some f -> f)
-			  ()
-			in
-			let sb = GBin.scrolled_window
-			  ~packing:w#add ()
-			in
-			let nv = GText.view
-			  ~buffer:p.script#buffer
-			  ~packing:sb#add
-			  ()
-			in
-			  nv#misc#modify_font
-			    current.text_font;
-			  ignore (w#connect#destroy
-				    ~callback:
-				    (fun () -> p.analyzed_view#remove_detached_view w));
-			  p.analyzed_view#add_detached_view w));
+	~callback:detach_view
     ];
     GAction.add_actions help_actions [
       GAction.add_action "Help" ~label:"_Help";