001: /* $Id: ResourceManager.java,v 1.52 2001/07/22 07:04:24 smulloni Exp $
002: * Time-stamp: <01/07/22 01:32:47 smulloni>
003: *
004: * Copyright (c) 2000 - 2001, Jacob Smullyan.
005: *
006: * This is part of SkunkDAV, a WebDAV client. See http://skunkdav.sourceforge.net/
007: * for the latest version.
008: *
009: * SkunkDAV is free software; you can redistribute it and/or
010: * modify it under the terms of the GNU General Public License as published
011: * by the Free Software Foundation; either version 2, or (at your option)
012: * any later version.
013: *
014: * SkunkDAV is distributed in the hope that it will be useful,
015: * but WITHOUT ANY WARRANTY; without even the implied warranty of
016: * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
017: * General Public License for more details.
018: *
019: * You should have received a copy of the GNU General Public License
020: * along with SkunkDAV; see the file COPYING. If not, write to the Free
021: * Software Foundation, 59 Temple Place - Suite 330, Boston, MA
022: * 02111-1307, USA.
023: */
024:
025: package org.skunk.dav.client.gui;
026:
027: import java.text.MessageFormat;
028: import java.util.MissingResourceException;
029: import java.util.ResourceBundle;
030: import javax.swing.ImageIcon;
031: import org.skunk.trace.Debug;
032:
033: public class ResourceManager {
034: private static ResourceBundle bundle;
035: //it's rather annoying that I didn't stick with a naming convention here. Will have to clean this up. TO BE DONE.
036: public static final String EXPLORER_RESOURCE_BUNDLE = "org.skunk.dav.client.gui.explorer";
037: public static final String EXPLORER_NAME = "explorer_name";
038: public static final String VIEW_KEY = "view";
039: public static final String CLOSE_KEY = "close";
040: public static final String EXIT_KEY = "exit";
041: public static final String FILE_KEY = "file";
042: public static final String HELP_KEY = "help";
043: public static final String EDIT_KEY = "edit";
044: public static final String OPEN_KEY = "open";
045: public static final String CONNECT_KEY = "connect";
046: public static final String SAVE_KEY = "save";
047: public static final String SAVE_AS_KEY = "save_as";
048: public static final String COPY_KEY = "copy";
049: public static final String MOVE_KEY = "move";
050: public static final String DELETE_KEY = "delete";
051: public static final String LOCK_KEY = "lock";
052: public static final String UNLOCK_KEY = "unlock";
053: public static final String VIEW_PROPERTIES_KEY = "view_properties";
054: public static final String PROPERTIES_KEY = "properties";
055: public static final String REFRESH_KEY = "refresh";
056: public static final String NEW_COLLECTION_KEY = "new_collection";
057: public static final String ABOUT_SPI_KEY = "about_spi";
058: public static final String LOGIN_KEY = "login";
059: public static final String LOGIN_NAME_KEY = "login_name";
060: public static final String PASSWORD_KEY = "password";
061: public static final String ADD_CONNECTION_TITLE = "add_connection_title";
062: public static final String ADD_CONNECTION_PROMPT = "add_connection_prompt";
063: public static final String ADD_NEW_CONNECTION_LABEL = "add_new_connection_label";
064: public static final String ADD_CONNECTION_LABEL = "add_connection_label";
065: public static final String REMOVE_CONNECTION_TITLE = "remove_connection_title";
066: public static final String REMOVE_CONNECTION_PROMPT = "remove_connection_prompt";
067: public static final String REMOVE_CONNECTION_LABEL = "remove_connection_label";
068: public static final String NEW_FILE_KEY = "new_file";
069: public static final String CONNECTION_PROMPT = "connection_prompt";
070: public static final String HOST_PROMPT = "host_prompt";
071: public static final String PORT_PROMPT = "port_prompt";
072: public static final String PATH_PROMPT = "path_prompt";
073: public static final String USERNAME_PROMPT = "username_prompt";
074: public static final String PASSWORD_PROMPT = "password_prompt";
075: public static final String REMEMBER_PASSWORD_PROMPT = "remember_password_prompt";
076: public static final String OK = "ok";
077: public static final String CANCEL = "cancel";
078: public static final String ROOT_NODE_LABEL = "root_node_label";
079: public static final String DISCONNECTION_KEY = "disconnection";
080: public static final String DISCONNECTION_ERROR_MESSAGE = "disconnection_error_message";
081: public static final String DISCONNECTION_ERROR_TITLE = "disconnection_error_title";
082: public static final String NEW_COLLECTION_PROMPT = "new_collection_prompt";
083: public static final String NEW_COLLECTION_DIALOG_TITLE = "new_collection_dialog_title";
084: public static final String ERROR_DIALOG_TITLE = "error_dialog_title";
085: public static final String NEW_COLLECTION_ERROR_MESSAGE = "new_collection_error_message";
086: public static final String STATUS_ERROR_MESSAGE = "status_error_message";
087: public static final String NEW_FILE_PROMPT = "new_file_prompt";
088: public static final String NEW_FILE_DIALOG_TITLE = "new_file_dialog_title";
089: public static final String CONNECTION_ERROR_MESSAGE = "connection_error_message";
090: public static final String DELETE_ERROR_MESSAGE = "delete_error_message";
091: public static final String COPY_DIALOG_MESSAGE = "copy_dialog_message";
092: public static final String COPY_DIALOG_TITLE = "copy_dialog_title";
093: public static final String MOVE_DIALOG_MESSAGE = "move_dialog_message";
094: public static final String MOVE_DIALOG_TITLE = "move_dialog_title";
095: public static final String INVALID_DESTINATION_ERROR_MESSAGE = "invalid_destination_error_message";
096: public static final String PROPERTIES_DIALOG_TITLE = "properties_dialog_title";
097: public static final String DAV_PROPERTIES_TAB_TITLE = "dav_properties_tab_title";
098: public static final String CUSTOM_PROPERTIES_TAB_TITLE = "custom_properties_tab_title";
099: public static final String HOST_FILE_PROP = "host_file_prop";
100: public static final String PORT_FILE_PROP = "port_file_prop";
101: public static final String FILE_NAME_FILE_PROP = "file_name_file_prop";
102: public static final String CREATION_DATE_FILE_PROP = "creation_date_file_prop";
103: public static final String LAST_MODIFIED_FILE_PROP = "last_modified_file_prop";
104: public static final String CONTENT_TYPE_FILE_PROP = "content_type_file_prop";
105: public static final String CONTENT_LENGTH_FILE_PROP = "content_length_file_prop";
106: public static final String CONTENT_LANGUAGE_FILE_PROP = "content_language_file_prop";
107: public static final String DISPLAY_NAME_FILE_PROP = "display_name_file_prop";
108: public static final String RESOURCE_TYPE_FILE_PROP = "resource_type_file_prop";
109: public static final String ETAG_FILE_PROP = "etag_file_prop";
110: public static final String SUPPORTED_LOCKS_FILE_PROP = "supported_locks_file_prop";
111: public static final String ACTIVE_LOCKS_FILE_PROP = "active_locks_file_prop";
112: public static final String LINKS_FILE_PROP = "links_file_prop";
113: public static final String NAME = "name";
114: public static final String NAMESPACE = "namespace";
115: public static final String VALUE = "value";
116: public static final String UPLOAD_KEY = "upload";
117: public static final String DOWNLOAD_KEY = "download";
118: public static final String DOWNLOAD_SUCCESS_MESSAGE = "download_success_message";
119: public static final String DOWNLOAD_SUCCESS_DIALOG_TITLE = "download_success_dialog_title";
120: public static final String UPLOAD_CHOOSER_DIALOG_TITLE = "upload_chooser_dialog_title";
121: public static final String DOWNLOAD_CHOOSER_DIALOG_TITLE = "download_chooser_dialog_title";
122: public static final String COPY_CHOOSER_DIALOG_TITLE = "copy_chooser_dialog_title";
123: public static final String MOVE_CHOOSER_DIALOG_TITLE = "move_chooser_dialog_title";
124: public static final String TRY = "try";
125: public static final String REVERT = "revert";
126: public static final String DEFAULT = "default";
127: public static final String PREFERENCES_KEY = "preferences";
128: public static final String TABLE_VIEW_CUSTOMIZER_BORDER_TITLE = "table_view_customizer_border_title";
129: public static final String TABLE_VIEW_CUSTOMIZER_TITLE = "table_view_customizer_title";
130: public static final String TABLE_VIEW_SOURCE_LIST_TITLE = "table_view_source_list_title";
131: public static final String TABLE_VIEW_SINK_LIST_TITLE = "table_view_sink_list_title";
132: public static final String RENAME_DIALOG_TITLE = "rename_dialog_title";
133: public static final String RENAME_DIALOG_MESSAGE = "rename_dialog_message";
134: public static final String RENAME_KEY = "rename";
135: public static final String PUT_NOT_ALLOWED_MESSAGE = "put_not_allowed_message";
136: public static final String STEAL_LOCK_KEY = "steal_lock_key";
137: public static final String ADD_KEY = "add";
138: public static final String PROPERTY_NAME = "property_name";
139: public static final String PROPERTY_VALUE = "property_value";
140: public static final String PROPERTY_NAMESPACE = "property_namespace";
141: public static final String PROPERTY_ADD_DIALOG_TITLE = "property_add_dialog_title";
142: public static final String PROPERTY_EDIT_DIALOG_TITLE = "property_edit_dialog_title";
143: public static final String CLOSE_BUFFER_KEY = "close_buffer";
144: public static final String CLOSE_DIRTY_BUFFER_WARNING = "close_dirty_buffer_warning";
145: public static final String UNDO_KEY = "undo";
146: public static final String REDO_KEY = "redo";
147: public static final String CUT_KEY = "cut";
148: public static final String COPY_TEXT_KEY = "copy_text"; //to avoid collision with COPY_KEY, above
149: public static final String PASTE_KEY = "paste";
150: public static final String SELECT_ALL_KEY = "select_all";
151: public static final String SEARCH_KEY = "search";
152: public static final String REPLACE_KEY = "replace";
153: public static final String GOTO_LINE_KEY = "goto_line";
154: public static final String LINE_AND_COLUMN = "line_and_column";
155: public static final String FIND_PROMPT = "find_prompt";
156: public static final String REVERSE_OPTION = "reverse_option";
157: public static final String LITERAL_OPTION = "literal_option";
158: public static final String CASE_OPTION = "case_option";
159: public static final String REGEXP_OPTION = "regexp_option";
160: public static final String INCREMENTAL_OPTION = "incremental_option";
161: public static final String WRAPPED_OPTION = "wrapped_option";
162: public static final String FIND_NEXT_OPTION = "find_next_option";
163: public static final String REPLACE_OPTION = "replace_option";
164: public static final String REPLACE_ALL_OPTION = "replace_all_option";
165: public static final String REPLACE_WITH_PROMPT = "replace_with_prompt";
166: public static final String SEARCH_FAILED_MESSAGE = "search_failed_message";
167: public static final String SEARCH_FAILED_TITLE = "search_failed_title";
168: public static final String GOTO_LINE_PROMPT = "goto_line_prompt";
169: public static final String IMAGE_DESCRIPTION = "image_description";
170: public static final String REPLACE_PROMPT = "replace_prompt";
171: public static final String REPLACE_TITLE = "replace_title";
172: public static final String END_REPLACE_TITLE = "end_replace_title";
173: public static final String END_REPLACE_MESSAGE = "end_replace_message";
174: public static final String WORD_WRAP_KEY = "word_wrap";
175: public static final String PROTOCOL_PROMPT = "protocol_prompt";
176: public static final String DIRTY_BUFFER_ON_EXIT_MESSAGE = "dirty_buffer_on_exit_message";
177: public static final String DIRTY_BUFFER_ON_EXIT_TITLE = "dirty_buffer_on_exit_title";
178: public static final String ABOUT_KEY = "about";
179: public static final String CONNECTION_DIALOG_TITLE = "connection_dialog_title";
180: public static final String CONNECTION_DIALOG_PROMPT = "connection_dialog_prompt";
181: public static final String CONNECTION_PARSE_ERROR_MESSAGE = "connection_parse_error_message";
182: public static final String CONNECT_PREVIOUS_KEY = "connect_previous";
183: public static final String NETWORK_CUSTOMIZER_TIMEOUT_TITLE = "network_customizer_timeout_title";
184: public static final String TIMEOUT_BORDER_TITLE = "timeout_border_title";
185: public static final String SERVER_BORDER_TITLE = "server_border_title";
186: public static final String NETWORK_CUSTOMIZER_TITLE = "network_customizer_title";
187: public static final String GLOBAL_PROPERTIES = "global_properties";
188: public static final String GLOBAL_BACKGROUND = "global_background";
189: public static final String GLOBAL_FOREGROUND = "global_foreground";
190: public static final String GLOBAL_CARET_COLOR = "global_caret_color";
191: public static final String FONT_NAME = "font_name";
192: public static final String FONT_SIZE = "font_size";
193: public static final String FILE_MODE_PROPERTIES = "file_mode_properties";
194: public static final String FILE_MODES = "file_modes";
195: public static final String EXTENSIONS = "extensions";
196: public static final String ADD_EXTENSION = "add_extension";
197: public static final String REMOVE_EXTENSION = "remove_extension";
198: public static final String HIGHLIGHT_THIS_MODE = "highlight_this_mode";
199: public static final String NEW_EXTENSION_DIALOG_TITLE = "new_extension_dialog_title";
200: public static final String NEW_EXTENSION_DIALOG_PROMPT = "new_extension_dialog_prompt";
201: public static final String SYNTAX_HIGHLIGHTING_STYLES = "syntax_highlighting_styles";
202: public static final String STYLE_PROPERTIES = "style_properties";
203: public static final String BOLD = "bold";
204: public static final String ITALIC = "italic";
205: public static final String COLOR = "color";
206: public static final String PREVIEW = "preview";
207: public static final String TAB_SIZE = "tab_size";
208: public static final String LINE_SEPARATOR = "line_separator";
209: public static final String CR_LINE_SEPARATOR = "cr_line_separator";
210: public static final String LF_LINE_SEPARATOR = "lf_line_separator";
211: public static final String CRLF_LINE_SEPARATOR = "crlf_line_separator";
212: public static final String TEXT_EDITOR_CUSTOMIZER_TITLE = "text_editor_customizer_title";
213: public static final String SYNTAX_HIGHLIGHT_KEY = "syntax_highlight";
214: public static final String TEXT_EDITOR_CUSTOMIZER_IO_EXCEPTION = "text_editor_customizer_io_exception";
215: public static final String LOCK_OWNER_PROMPT = "lock_owner_prompt";
216: public static final String LOCK_OWNER_DIALOG_TITLE = "lock_owner_dialog_title";
217: public static final String OWNER_PROMPT = "owner_prompt";
218: public static final String SERVERS_LABEL = "servers_label";
219: public static final String ADD_SERVER_LABEL = "add_server_label";
220: public static final String DEL_SERVER_LABEL = "del_server_label";
221: public static final String HTTPS_NOT_SUPPORTED_MESSAGE = "https_not_supported_message";
222: public static final String HTTPS_NOT_SUPPORTED_DIALOG_TITLE = "https_not_supported_dialog_title";
223: public static final String PORT_INVALID_MESSAGE = "port_invalid_message";
224: public static final String PORT_INVALID_TITLE = "port_invalid_title";
225: public static final String REMEMBER_PASSWORD_LABEL = "remember_password_label";
226: public static final String ADD_MESSAGE = "add_message";
227: public static final String REMOVE_MESSAGE = "remove_message";
228: public static final String RENAME_MESSAGE = "rename_message";
229: public static final String KEY = "key";
230: public static final String MESSAGE = "message";
231: public static final String NEW_MESSAGE_PROMPT = "new_message_prompt";
232: public static final String CANNOT_OPEN = "cannot_open";
233: public static final String RENAME_MESSAGE_PROMPT = "rename_message_prompt";
234: public static final String LOGIN_TITLE = "login_title";
235: public static final String LOGIN_MESSAGE = "login_message";
236: public static final String RELEASE_VERSION = "release_version";
237:
238: /*
239: * IMAGE RESOURCES
240: */
241:
242: public static final String LOCK_ICON = "lock.gif";
243: public static final String NOLOCK_ICON = "nolock.gif";
244: public static final String FOLDER_ICON = "dir_close.gif";
245: public static final String OPEN_NODE_ICON = "dir_open.gif";
246: public static final String CLOSED_NODE_ICON = "dir_close.gif";
247: public static final String LEAF_NODE_ICON = "dir_close.gif";
248: public static final String EXPANDED_ICON = "expanded.gif";
249: public static final String COLLAPSED_ICON = "collapsed.gif";
250: public static final String SPLASH_SCREEN_ICON = "splash.gif";
251: public static final String SPLASH_SCREEN_TEXT = "splash_screen_text";
252:
253: static {
254: try {
255: bundle = ResourceBundle.getBundle(EXPLORER_RESOURCE_BUNDLE);
256: } catch (MissingResourceException missOrEx) {
257: Debug.trace(ResourceManager.class, Debug.DP2, missOrEx);
258: }
259: }
260:
261: public static String getMessage(String key) {
262: return (bundle == null) ? null : bundle.getString(key);
263: }
264:
265: public static String getMessage(String key, int minimumLength) {
266: return pad(getMessage(key), minimumLength);
267: }
268:
269: public static String getMessage(String key, String defaultMessage) {
270: String message = getMessage(key);
271: return (message == null) ? defaultMessage : message;
272: }
273:
274: public static String getMessage(String key, String defaultMessage,
275: int minimumLength) {
276: return pad(getMessage(key, defaultMessage), minimumLength);
277: }
278:
279: public static String getMessage(String key, Object[] interpolations) {
280: String formattedMessage = getMessage(key);
281: return MessageFormat.format(formattedMessage, interpolations);
282: }
283:
284: public static String getMessage(String key, String defaultMessage,
285: Object[] interpolations) {
286: String formattedMessage = getMessage(key, defaultMessage);
287: return MessageFormat.format(formattedMessage, interpolations);
288: }
289:
290: public static String getMessage(String key, String defaultMessage,
291: int minimumLength, Object[] interpolations) {
292: return pad(getMessage(key, defaultMessage, interpolations),
293: minimumLength);
294: }
295:
296: public static String getMessage(String key, int minimumLength,
297: Object[] interpolations) {
298: return pad(getMessage(key, interpolations), minimumLength);
299: }
300:
301: public static ImageIcon getImageIcon(String key,
302: String descriptionKey) {
303: String description = (descriptionKey == null) ? null
304: : getMessage(descriptionKey, descriptionKey);
305: ImageIcon ii = new ImageIcon(ResourceManager.class
306: .getResource(findImageResource(key)));
307: if (description != null)
308: ii.setDescription(description);
309: return ii;
310: }
311:
312: public static ImageIcon getImageIcon(String key) {
313: return new ImageIcon(ResourceManager.class
314: .getResource(findImageResource(key)));
315: }
316:
317: public static String pad(String s, int length) {
318: if (s == null)
319: s = "";
320: int curlen = s.length();
321: if (length <= curlen)
322: return s;
323: StringBuffer sb = new StringBuffer(length);
324: int diff = length - curlen;
325: char[] whitespace = new char[diff];
326: for (int i = 0; i < diff; i++)
327: whitespace[i] = ' ';
328: sb.append(s).append(whitespace);
329: return sb.toString();
330: }
331:
332: private static String findImageResource(String key) {
333: return "/images/" + key;
334: }
335: }
336:
337: /* $Log: ResourceManager.java,v $
338: /* Revision 1.52 2001/07/22 07:04:24 smulloni
339: /* changed the handling of release number.
340: /*
341: /* Revision 1.51 2001/07/15 02:55:23 smulloni
342: /* fixed some strings in DAVAuthenticatorImpl which were hardcoded;
343: /* moved javadocs from /doc to /docs/api
344: /*
345: /* Revision 1.50 2001/07/11 02:15:01 smulloni
346: /* the previous spi build targets have been folded into the main build;
347: /* also added a javadoc target.
348: /*
349: /* Revision 1.49 2001/06/13 01:09:03 smulloni
350: /* Some improvements to the network customizer (which is still buggy).
351: /* Also improvements for using the doAllprop switch, and for the layout of
352: /* the PropertiesDialog.
353: /*
354: /* Revision 1.48 2001/06/09 03:09:09 smulloni
355: /* added server customization to the NetworkCustomizer. Buggy.
356: /*
357: /* Revision 1.47 2001/05/31 02:14:37 smulloni
358: /* started draft of server configuration panel.
359: /*
360: /* Revision 1.46 2001/05/30 15:25:28 smulloni
361: /* Added prompt for lock owner the first time a resource is locked for a
362: /* given server -- default value is username, if any.
363: /*
364: /* Revision 1.45 2001/05/30 03:49:35 smulloni
365: /* Some bug fixes and improvements to authentication handling. Users are now
366: /* prompted for a password the first time they connect to a given server
367: /* in a session; if the password is rejected, they are asked again.
368: /* Users also now have the option of whether a given password will be remembered
369: /* or not.
370: /*
371: /* Revision 1.44 2001/02/16 18:15:10 smulloni
372: /* many fixes to TextEditorCustomizer. FileMode and SyntaxStyle now have a
373: /* configData property (they will probably be made into sibling classes).
374: /*
375: /* Revision 1.43 2001/02/06 22:13:40 smulloni
376: /* first more-or-less working version of syntax highlighting, with customization.
377: /*
378: /* Revision 1.42 2001/02/02 23:30:33 smulloni
379: /* adding customization features to the text editor.
380: /*
381: /* Revision 1.41 2001/01/23 20:50:09 smulloni
382: /* added configurable socket timeout
383: /*
384: /* Revision 1.40 2001/01/05 08:01:12 smulloni
385: /* changes to the connection gui for the Explorer; added depth configurability to
386: /* propfind in the jpython test script; added an experimental "allprop" system
387: /* property which affects the propfind query type
388: /*
389: /* Revision 1.39 2000/12/21 18:53:13 smulloni
390: /* cosmetic improvements.
391: /*
392: /* Revision 1.38 2000/12/19 22:06:15 smulloni
393: /* adding documentation.
394: /*
395: /* Revision 1.37 2000/12/19 20:17:54 smulloni
396: /* added an "About..." menu item.
397: /*
398: /* Revision 1.36 2000/12/19 19:22:22 smulloni
399: /* some tweaks: ExitAction now cleans up the app's buffers. The app now does
400: /* not resize every time a buffer is added or removed.
401: /*
402: /* Revision 1.35 2000/12/18 23:22:47 smulloni
403: /* added optional SSL capability to the gui application. Separate make targets
404: /* exist for building it will SSL support.
405: /*
406: /* Revision 1.34 2000/12/15 23:22:08 smulloni
407: /* added word wrap to text editor.
408: /*
409: /* Revision 1.33 2000/12/14 06:36:26 smulloni
410: /* changes to search and replace in text editor.
411: /*
412: /* Revision 1.32 2000/12/08 22:25:06 smulloni
413: /* added non-incremental search, and forward and reverse regex search, using
414: /* the org.apache.oro regex package.
415: /*
416: /* Revision 1.31 2000/12/07 00:01:34 smulloni
417: /* adding an additional editor, still hard-coded into the DAVEditorFactory.
418: /*
419: /* Revision 1.30 2000/12/04 23:51:16 smulloni
420: /* added ImageViewer; fixed word in SimpleTextEditor
421: /*
422: /* Revision 1.29 2000/12/03 23:53:26 smulloni
423: /* added license and copyright preamble to java files.
424: /*
425: /* Revision 1.28 2000/12/01 16:25:53 smullyan
426: /* improvements to look and feel; fixed NPE in DAVFile; new actions for text
427: /* editor
428: /*
429: /* Revision 1.27 2000/11/29 23:16:04 smullyan
430: /* adding first rough cut of search capability to the text editor. View
431: /* is being updated to allow components to be docked into the status bar.
432: /*
433: /* Revision 1.26 2000/11/28 00:01:38 smullyan
434: /* added a status bar/minibuffer, with a location field showing the current line and
435: /* column number (for the SimpleTextEditor and kin only).
436: /*
437: /* Revision 1.25 2000/11/20 23:30:21 smullyan
438: /* more editor integration work.
439: /*
440: /* Revision 1.24 2000/11/16 20:45:18 smullyan
441: /* the start of editor integration.
442: /*
443: /* Revision 1.23 2000/11/15 20:17:03 smullyan
444: /* added a Buffer interface, which is a wrapper around a displayable component.
445: /*
446: /* Revision 1.22 2000/11/13 23:28:31 smullyan
447: /* first pass at a gui for proppatch, added to the propertiese dialog. Highly
448: /* problematic still, needs substantial work.
449: /*
450: /* Revision 1.21 2000/11/10 22:40:07 smullyan
451: /* added icon to table for resource type; fixes to copy and move; disabling of
452: /* menu items that are inappropriate.
453: /*
454: /* Revision 1.20 2000/11/09 23:34:59 smullyan
455: /* log added to every Java file, with the help of python. Lock stealing
456: /* implemented, and treatment of locks made more robust.
457: /* */
|