diff options
| -rw-r--r-- | ide/coqide.ml | 68 |
1 files changed, 27 insertions, 41 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 75a5c5ae33..0fac50abe8 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"; |