~azzar1/unity/add-show-desktop-key

« back to all changes in this revision

Viewing changes to www/media/console/console.js

  • Committer: mattgiuca
  • Date: 2008-01-31 05:13:17 UTC
  • Revision ID: svn-v3-trunk0:2b9c9e99-6f39-0410-b283-7f802c844ae2:trunk:350
media/console/console.js: Rewrote console history storage, browsing, and
updating algorithm. This fixes usability problems with the old one (it didn't
store the current line, for instance).
The new algorithm lets you edit historical items and remembers all edits until
you press return. This mimics the GNU Readline algorithm as closely as I can
tell.

Show diffs side-by-side

added added

removed removed

Lines of Context:
105
105
 
106
106
var magic = 'xyzzy';
107
107
 
108
 
function historyUp()
 
108
/* current_text is the string currently on the command line.
 
109
 * If non-empty, it will be stored at the bottom of the history.
 
110
 */
 
111
function historyUp(current_text)
109
112
{
110
 
    if (this.cursor >= 0)
 
113
    /* Remember the changes made to this item */
 
114
    this.edited[this.cursor] = current_text;
 
115
    if (this.cursor > 0)
111
116
    {
112
117
        this.cursor--;
113
118
    }
 
119
    this.earliestCursor = this.cursor;
114
120
}
115
121
 
116
 
function historyDown()
 
122
function historyDown(current_text)
117
123
{
118
 
    if (this.cursor < this.items.length)
 
124
    /* Remember the changes made to this item */
 
125
    this.edited[this.cursor] = current_text;
 
126
    if (this.cursor < this.items.length - 1)
119
127
    {
120
128
        this.cursor++;
121
129
    }
123
131
 
124
132
function historyCurr()
125
133
{
126
 
    if (this.cursor < 0 || this.cursor >= this.items.length)
127
 
    {
128
 
        return "";
129
 
    }
130
 
    return this.items[this.cursor];
 
134
    return this.edited[this.cursor];
131
135
}
132
136
 
133
 
function historyAdd(text)
 
137
function historySubmit(text)
134
138
{
135
 
    this.items[this.items.length] = text;
136
 
    this.cursor = this.items.length;
 
139
    /* Copy the selected item's "edited" version over the permanent version of
 
140
     * the last item. */
 
141
    this.items[this.items.length-1] = text;
 
142
    /* Add a new blank item */
 
143
    this.items[this.items.length] = "";
 
144
    this.cursor = this.items.length-1;
 
145
    /* Blow away all the edited versions, replacing them with the existing
 
146
     * items set.
 
147
     * Not the whole history - just start from the earliest edited one.
 
148
     * (This avoids slowdown over extended usage time).
 
149
     */
 
150
    for (var i=this.earliestCursor; i<=this.cursor; i++)
 
151
        this.edited[i] = this.items[i];
 
152
    this.earliestCursor = this.cursor;
137
153
}
138
154
 
139
155
function historyShow()
140
156
{
141
157
    var res = "";
142
 
    if (this.cursor == -1)
143
 
    {
144
 
        res += "[]";
145
 
    }
146
158
    for (var i = 0; i < this.items.length; i++)
147
159
    {
148
160
        if (i == this.cursor)
163
175
    return res;
164
176
}
165
177
 
 
178
/* How history works
 
179
 * This is a fairly complex mechanism due to complications when editing
 
180
 * history items. We store two arrays. "items" is the permanent history of
 
181
 * each item. "edited" is a "volatile" version of items - the edits made to
 
182
 * the history between now and last time you hit "enter".
 
183
 * This is because the user can go back and edit any of the previous items,
 
184
 * and the edits are remembered until they hit enter.
 
185
 *
 
186
 * When hitting enter, the "edited" version of the currently selected item
 
187
 * replaces the "item" version of the last item in the list.
 
188
 * Then a new blank item is created, for the new line of input.
 
189
 * Lastly, all the "edited" versions are replaced with their stable versions.
 
190
 *
 
191
 * Cursor never points to an invalid location.
 
192
 */
166
193
function History()
167
194
{
168
 
    this.items = new Array();
169
 
    this.cursor = -1;
 
195
    this.items = new Array("");
 
196
    this.edited = new Array("");
 
197
    this.cursor = 0;
 
198
    this.earliestCursor = 0;
170
199
    this.up = historyUp;
171
200
    this.down = historyDown;
172
201
    this.curr = historyCurr;
173
 
    this.add = historyAdd;
 
202
    this.submit = historySubmit;
174
203
    this.show = historyShow;
175
204
}
176
205
 
287
316
    case 13:                /* Enter key */
288
317
        /* Send the line of text to the server */
289
318
        console_enter_line(inp.value);
290
 
        hist.add(inp.value);
 
319
        hist.submit(inp.value);
291
320
        inp.value = hist.curr();
292
321
        break;
293
322
    case 38:                /* Up arrow */
294
 
        hist.up();
 
323
        hist.up(inp.value);
295
324
        inp.value = hist.curr();
296
325
        break;
297
326
    case 40:                /* Down arrow */
298
 
        hist.down();
 
327
        hist.down(inp.value);
299
328
        inp.value = hist.curr();
300
329
        break;
301
330
    }