Allowing proof view to be detached in CoqIDE.

5 files changed, 67 insertions, 36 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index d53d288d7..783f4b431 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -653,24 +653,7 @@ end
 
 module MiscMenu = struct
 
-let detach_view sn =
-  (* Open a separate window containing the current buffer *)
-  let file = match sn.fileops#filename with
-    |None -> "*scratch*"
-    |Some f -> f
-  in
-  let w = GWindow.window ~show:true ~title:file ~position:`CENTER
-    ~width:(prefs.window_width*2/3)
-    ~height:(prefs.window_height*2/3)
-    ()
-  in
-  let sb = GBin.scrolled_window ~packing:w#add ()
-  in
-  let nv = GText.view ~buffer:sn.buffer ~packing:sb#add ()
-  in
-  nv#misc#modify_font prefs.text_font;
-  (* If the buffer in the main window is closed, destroy this detached view *)
-  ignore (sn.script#connect#destroy ~callback:w#destroy)
+let detach_view sn = sn.control#detach ()
 
 let detach_view = cb_on_current_term detach_view
 
diff --git a/ide/session.ml b/ide/session.ml
index bb23ed58a..f42feae0c 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -20,6 +20,11 @@ class type ['a] page =
     method on_update : callback:('a -> unit) -> unit
   end
 
+class type control =
+  object
+    method detach : unit -> unit
+  end
+
 type errpage = (int * string) list page
 type jobpage = string Int.Map.t page
 
@@ -36,6 +41,7 @@ type session = {
   tab_label : GMisc.label;
   errpage : errpage;
   jobpage : jobpage;
+  mutable control : control;
 }
 
 let create_buffer () =
@@ -340,6 +346,11 @@ let create_messages () =
   let _ = messages#misc#set_can_focus true in
   messages
 
+let dummy_control : control =
+  object
+    method detach () = ()
+  end
+
 let create file coqtop_args =
   let basename = match file with
     |None -> "*scratch*"
@@ -374,7 +385,8 @@ let create file coqtop_args =
     finder=finder;
     tab_label= GMisc.label ~text:basename ();
     errpage=errpage;
-    jobpage=jobpage
+    jobpage=jobpage;
+    control = dummy_control;
   }
 
 let kill (sn:session) =
@@ -390,6 +402,9 @@ let build_layout (sn:session) =
   let session_box =
     GPack.vbox ~packing:(session_paned#pack1 ~shrink:false ~resize:true) ()
   in
+
+  (** Right part of the window. *)
+
   let eval_paned = GPack.paned `HORIZONTAL ~border_width:5
     ~packing:(session_box#pack ~expand:true) () in
   let script_frame = GBin.frame ~shadow_type:`IN
@@ -398,10 +413,25 @@ let build_layout (sn:session) =
     ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:script_frame#add () in
   let state_paned = GPack.paned `VERTICAL
     ~packing:eval_paned#add2 () in
-  let proof_frame = GBin.frame ~shadow_type:`IN
-    ~packing:state_paned#add1 () in
+
+  (** Proof buffer. *)
+
+  let title = Printf.sprintf "Proof (%s)" sn.tab_label#text in
+  let proof_detachable = Wg_Detachable.detachable ~title () in
+  let () = proof_detachable#button#misc#hide () in
+  let () = proof_detachable#frame#set_shadow_type `IN in
+  let () = state_paned#add1 proof_detachable#coerce in
+  let callback _ = proof_detachable#show in
+  let () = proof_detachable#connect#attached ~callback in
+  let callback _ =
+    sn.proof#coerce#misc#set_size_request ~width:500 ~height:400 ()
+  in
+  let () = proof_detachable#connect#detached ~callback in
   let proof_scroll = GBin.scrolled_window
-    ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:proof_frame#add () in
+    ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:proof_detachable#pack () in
+
+  (** Message buffer. *)
+
   let message_frame = GPack.notebook ~packing:state_paned#add () in
   let add_msg_page pos name text (w : GObj.widget) =
     let detachable =
@@ -468,4 +498,10 @@ let build_layout (sn:session) =
   img#set_stock `YES;
   eval_paned#set_position 1;
   state_paned#set_position 1;
+  let control =
+    object
+      method detach () = proof_detachable#detach ()
+    end
+  in
+  let () = sn.control <- control in
   (Some session_tab#coerce,None,session_paned#coerce)
diff --git a/ide/session.mli b/ide/session.mli
index 527e1d170..925b13567 100644
--- a/ide/session.mli
+++ b/ide/session.mli
@@ -16,6 +16,11 @@ class type ['a] page =
     method on_update : callback:('a -> unit) -> unit
   end
 
+class type control =
+  object
+    method detach : unit -> unit
+  end
+
 type errpage = (int * string) list page
 type jobpage = string Int.Map.t page
 
@@ -32,6 +37,7 @@ type session = {
   tab_label : GMisc.label;
   errpage : errpage;
   jobpage : jobpage;
+  mutable control : control;
 }
 
 (** [create filename coqtop_args] *)
diff --git a/ide/wg_Detachable.ml b/ide/wg_Detachable.ml
index e2c2311f4..9eb1b3232 100644
--- a/ide/wg_Detachable.ml
+++ b/ide/wg_Detachable.ml
@@ -50,8 +50,23 @@ class detachable (obj : ([> Gtk.box] as 'a) Gobject.obj) =
 
     method visible = win#misc#visible || self#misc#visible
 
+    method frame = frame
+
     method button = but
 
+    method attach () =
+      win#misc#hide ();
+      frame#misc#reparent self#coerce;
+      detached <- false;
+      attached_cb self#child
+
+    method detach () =
+      frame#misc#reparent win#coerce;
+      self#misc#hide ();
+      win#present ();
+      detached <- true;
+      detached_cb self#child
+
     initializer
       self#set_homogeneous false;
       super#pack ~expand:false but#coerce;
@@ -59,19 +74,8 @@ class detachable (obj : ([> Gtk.box] as 'a) Gobject.obj) =
       win#misc#hide ();
       but#add (GMisc.label
         ~markup:"<span size='x-small'>D\nE\nT\nA\nC\nH</span>" ())#coerce;
-      ignore(win#event#connect#delete ~callback:(fun _ ->
-        win#misc#hide ();
-        frame#misc#reparent self#coerce;
-        detached <- false;
-        attached_cb self#child;
-        true));
-      ignore(but#connect#clicked ~callback:(fun _ ->
-        frame#misc#reparent win#coerce;
-        self#misc#hide ();
-        win#present ();
-        detached <- true;
-        detached_cb self#child;
-        ))
+      ignore(win#event#connect#delete ~callback:(fun _ -> self#attach (); true));
+      ignore(but#connect#clicked ~callback:(fun _ -> self#detach ()))
 
   end
 
diff --git a/ide/wg_Detachable.mli b/ide/wg_Detachable.mli
index 8e4df52db..23fedac9c 100644
--- a/ide/wg_Detachable.mli
+++ b/ide/wg_Detachable.mli
@@ -25,7 +25,9 @@ class detachable : ([> Gtk.box] as 'a) Gobject.obj ->
     method title : string
     method set_title : string -> unit
     method button : GButton.button
-
+    method frame : GBin.frame
+    method detach : unit -> unit
+    method attach : unit -> unit
   end
 
 val detachable :