diff options
| author |  vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-07 15:35:35 +0000 |
|---|---|---|
| committer | vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-07 15:35:35 +0000 |
| commit | 8f4d0165f0a1be1b81ecab0356f7040423406c28 (patch) | |
| tree | 35f20819c07e3d68d02cf0864b9549b2c8783c0a /ide | |
| parent | 35159e8aa9bf33b4882bc7f17c2e363f769624c7 (diff) | |
Remove the "detach script windows" feature.
See bug #2173.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12567 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 25 |
1 files changed, 0 insertions, 25 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 734bdccdc..99b259308 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -3113,31 +3113,6 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); !current.show_toolbar <- not !current.show_toolbar; !show_toolbar !current.show_toolbar) in - let _ = configuration_factory#add_item - "Detach _Script Window" - ~callback: - (do_if_not_computing "detach script window" (sync - (fun () -> - let nb = session_notebook in - if nb#misc#toplevel#get_oid=w#coerce#get_oid then - begin - let nw = GWindow.window - ~width:(!current.window_width*2/3) - ~height:(!current.window_height*2/3) - ~position:`CENTER - ~wm_name:"CoqIde" - ~wm_class:"CoqIde" - ~title:"Script" - ~show:true () in - let parent = Option.get nb#misc#parent in - ignore (nw#connect#destroy - ~callback: - (fun () -> nb#misc#reparent parent)); - nw#add_accel_group accel_group; - nb#misc#reparent nw#coerce - end - ))) - in let _ = configuration_factory#add_item "Detach _View" |