+ /* File menu */
+ final static String open_command = "open";
+ final static String save_command = "save";
+ final static String export_command = "export";
+ final static String preferences_command = "preferences";
+ final static String close_command = "close";
+ final static String exit_command = "exit";
+
+ static final String[][] file_menu_entries = new String[][] {
+ { "Open", open_command },
+ { "Save a Copy", save_command },
+ { "Export Data", export_command },
+ { "Preferences", preferences_command },
+ { "Close", close_command },
+ { "Exit", exit_command },
+ };
+
+ /* Download menu */
+ final static String download_command = "download";
+ final static String download_label = "Download";
+