wg_Command: detachable, less "from the 80s", query pane

- Tabs have labels derived from the query (e.g. "About eq_ind" will have
  "eq_ind" as its label, that is better than "Page 1" ;-)
- Tabs have a [x] close icon
- Icon to create a new tab in in the notebook
- Dispotically grab the F1 key to open/close the query pane
  (alt-esc is grabbed by windows managers these days)
- Esc hides the query pane (like the search pane)
- F1 puts a detached query pane in front
- Tab switches from the combo-box to the entry on its right
- Detaching is taken-over, and the query pane is reparented in a regular
  window that can be resized
- A detached query pane can be put back by closing the window

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

1 files changed, 5 insertions, 7 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 5ff849268..cdd1a9e48 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -768,11 +768,9 @@ let coqtop_arguments sn =
 
 let coqtop_arguments = cb_on_current_term coqtop_arguments
 
-let show_query_pane sn =
+let show_hide_query_pane sn =
   let ccw = sn.command in
-  if ccw#frame#misc#visible
-  then ccw#frame#misc#hide ()
-  else ccw#frame#misc#show ()
+  if ccw#visible then ccw#hide else ccw#show
 
 let zoom_fit sn =
   let script = sn.script in
@@ -1058,9 +1056,9 @@ let build_ui () =
       ~callback:(fun _ ->
         prefs.show_toolbar <- not prefs.show_toolbar;
         !refresh_toolbar_hook ());
-    toggle_item "Show Query Pane" ~label:"Show _Query Pane"
-      ~accel:"<Alt>Escape"
-      ~callback:(cb_on_current_term MiscMenu.show_query_pane)
+    item "Query Pane" ~label:"_Query Pane"
+      ~accel:"F1"
+      ~callback:(cb_on_current_term MiscMenu.show_hide_query_pane)
   ];
   toggle_items view_menu Coq.PrintOpt.bool_items;