Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

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
  • Loading branch information...
commit cf59f30fc9a4f5e90805b54a4c6d39c9bbd96e65 1 parent d97cd41
letouzey authored
Showing with 27 additions and 41 deletions.
  1. +27 −41 ide/coqide.ml
68 ide/coqide.ml
View
@@ -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";
Please sign in to comment.
Something went wrong with that request. Please try again.