aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide_ui.ml
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-04-23 10:35:25 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-04-23 10:35:25 +0000
commitbd18c08212cbed9877167b64e0d1484a483b3cf6 (patch)
treec88bb9a6ae05ddecae3e9bd7d5a59c023c8ad6d1 /ide/coqide_ui.ml
parenta2e44a2dbe77c5ce227ea7e12d2cfce903221254 (diff)
Now CoqIDE has a nice find & replace mechanism. BTW, removing a blob of dead code that used to serve as such a long time ago.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15234 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqide_ui.ml')
-rw-r--r--ide/coqide_ui.ml7
1 files changed, 5 insertions, 2 deletions
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index eaf1e9348..6b464348c 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -20,6 +20,7 @@ let list_items menu li =
let init () =
let theui = Printf.sprintf "<ui>
+<accelerator action='Close Find' />
<menubar name='CoqIde MenuBar'>
<menu action='File'>
<menuitem action='New' />
@@ -48,8 +49,10 @@ let init () =
<menuitem action='Copy' />
<menuitem action='Paste' />
<separator />
- <menuitem action='Find in buffer' />
- <menuitem action='Find backwards' />
+ <menuitem action='Find' />
+ <menuitem action='Find Next' />
+ <menuitem action='Find Previous' />
+ <menuitem action='Replace' />
<menuitem action='Complete Word' />
<separator />
<menuitem action='External editor' />