← Back to branch summary

~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-07-15 07:19:34 UTC
  • Revision ID: svn-v3-trunk0:2b9c9e99-6f39-0410-b283-7f802c844ae2:trunk:875
Added "migrations" directory, which contains incremental database update
    scripts.
Updated users.sql, uniqueness key on offering table.
Added migration matching this update to the migrations directory. Mm handy!

Show diffs side-by-side

added added

removed removed

Lines of Context:
www/media/console/console.js
1
 
digest_constant = "hello";
2
 
 
3
 
var server_host;
4
 
var server_port;
5
 
var server_magic;
6
 
 
7
 
/* Starts the console server.
8
 
 * Returns an object with fields "host", "port", "magic" describing the
9
 
 * server.
10
 
 */
11
 
function start_server()
12
 
{
13
 
    var xhr = ajax_call("consoleservice", "start", {}, "POST");
14
 
    var json_text = xhr.responseText;
15
 
    return JSON.parse(json_text);
16
 
}
17
 
 
18
 
function onload()
19
 
{
20
 
    /* Start the server */
21
 
    var server_info = start_server();
22
 
    server_host = server_info.host;
23
 
    server_port = server_info.port;
24
 
    server_magic = server_info.magic;
25
 
}
26
 
 
27
 
/* Below here imported from trunk/console/console.js
28
 
 * (Tom Conway)
29
 
 */
30
 
 
31
 
var magic = 'xyzzy';
32
 
 
33
 
function historyUp()
34
 
{
35
 
    if (this.cursor >= 0)
 
1
/* IVLE - Informatics Virtual Learning Environment
 
2
 * Copyright (C) 2007-2008 The University of Melbourne
 
3
 *
 
4
 * This program is free software; you can redistribute it and/or modify
 
5
 * it under the terms of the GNU General Public License as published by
 
6
 * the Free Software Foundation; either version 2 of the License, or
 
7
 * (at your option) any later version.
 
8
 *
 
9
 * This program is distributed in the hope that it will be useful,
 
10
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 
11
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
12
 * GNU General Public License for more details.
 
13
 *
 
14
 * You should have received a copy of the GNU General Public License
 
15
 * along with this program; if not, write to the Free Software
 
16
 * Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA
 
17
 *
 
18
 * Module: Console (Client-side JavaScript)
 
19
 * Author: Tom Conway, Matt Giuca
 
20
 * Date: 30/1/2008
 
21
 */
 
22
 
 
23
var server_key;
 
24
 
 
25
/* Begin religious debate (tabs vs spaces) here: */
 
26
/* (This string will be inserted in the console when the user presses the Tab
 
27
 * key) */
 
28
TAB_STRING = "    ";
 
29
 
 
30
/* Console DOM objects */
 
31
console_body = null;
 
32
console_filler = null;
 
33
 
 
34
windowpane_mode = false;
 
35
server_started = false;
 
36
 
 
37
interrupted = false;
 
38
 
 
39
/* Starts the console server, if it isn't already.
 
40
 * This can be called any number of times - it only starts the one server.
 
41
 * Note that this is asynchronous. It will return after signalling to start
 
42
 * the server, but there is no guarantee that it has been started yet.
 
43
 * This is a separate step from console_init, as the server is only to be
 
44
 * started once the first command is entered.
 
45
 * Does not return a value. Writes to global variables
 
46
 * server_host, and server_port.
 
47
 *
 
48
 * \param callback Function which will be called after the server has been
 
49
 * started. No parameters are passed. May be null.
 
50
 */
 
51
function start_server(callback)
 
52
{
 
53
    if (server_started)
 
54
    {
 
55
        callback();
 
56
        return;
 
57
    }
 
58
    var callback1 = function(xhr)
 
59
        {
 
60
            var json_text = xhr.responseText;
 
61
            server_key = JSON.parse(json_text);
 
62
            server_started = true;
 
63
            if (callback != null)
 
64
                callback();
 
65
        }
 
66
 
 
67
    //var current_path;
 
68
    if(typeof(current_path) != 'undefined')
 
69
    {
 
70
        // We have a current_path - give a suggestion to the server
 
71
        var path;
 
72
        if (current_file.isdir)
 
73
        {
 
74
            // Browser
 
75
            path = path_join("/home", current_path);
 
76
        }
 
77
        else
 
78
        {
 
79
            // Editor - need to chop off filename
 
80
            var tmp_path = current_path.split('/');
 
81
            tmp_path.pop();
 
82
            path = path_join("/home", tmp_path.join('/'));
 
83
        }
 
84
        ajax_call(callback1, "consoleservice", "start", {"startdir": path}, "POST");
 
85
    }
 
86
    else
 
87
    {
 
88
        // No current_path - let the server decide
 
89
        ajax_call(callback1, "consoleservice", "start", {}, "POST");
 
90
    }
 
91
}
 
92
 
 
93
/** Initialises the console. All apps which import console are required to
 
94
 * call this function.
 
95
 * Optional "windowpane" (bool), if true, will cause the console to go into
 
96
 * "window pane" mode which will allow it to be opened and closed, and float
 
97
 * over the page.
 
98
 * (Defaults to closed).
 
99
 */
 
100
function console_init(windowpane)
 
101
{
 
102
    /* Set up the console as a floating pane */
 
103
    console_body = document.getElementById("console_body");
 
104
    /* If there is no console body, don't worry.
 
105
     * (This lets us import console.js even on pages without a console box */
 
106
    if (console_body == null) return;
 
107
    console_filler = document.getElementById("console_filler");
 
108
    if (windowpane)
 
109
    {
 
110
        windowpane_mode = true;
 
111
        console_minimize();
 
112
    }
 
113
}
 
114
 
 
115
/** Hide the main console panel, so the console minimizes to just an input box
 
116
 *  at the page bottom. */
 
117
function console_minimize()
 
118
{
 
119
    if (!windowpane_mode) return;
 
120
    console_body.setAttribute("class", "windowpane minimal");
 
121
    console_filler.setAttribute("class", "windowpane minimal");
 
122
}
 
123
 
 
124
/** Show the main console panel, so it enlarges out to its full size.
 
125
 */
 
126
function console_maximize()
 
127
{
 
128
    if (!windowpane_mode) return;
 
129
    console_body.setAttribute("class", "windowpane maximal");
 
130
    console_filler.setAttribute("class", "windowpane maximal");
 
131
}
 
132
 
 
133
/* current_text is the string currently on the command line.
 
134
 * If non-empty, it will be stored at the bottom of the history.
 
135
 */
 
136
function historyUp(current_text)
 
137
{
 
138
    /* Remember the changes made to this item */
 
139
    this.edited[this.cursor] = current_text;
 
140
    if (this.cursor > 0)
36
141
    {
37
142
        this.cursor--;
38
143
    }
 
144
    this.earliestCursor = this.cursor;
39
145
}
40
146
 
41
 
function historyDown()
 
147
function historyDown(current_text)
42
148
{
43
 
    if (this.cursor < this.items.length)
 
149
    /* Remember the changes made to this item */
 
150
    this.edited[this.cursor] = current_text;
 
151
    if (this.cursor < this.items.length - 1)
44
152
    {
45
153
        this.cursor++;
46
154
    }
48
156
 
49
157
function historyCurr()
50
158
{
51
 
    if (this.cursor < 0 || this.cursor >= this.items.length)
52
 
    {
53
 
        return "";
54
 
    }
55
 
    return this.items[this.cursor];
 
159
    return this.edited[this.cursor];
56
160
}
57
161
 
58
 
function historyAdd(text)
 
162
function historySubmit(text)
59
163
{
60
 
    this.items[this.items.length] = text;
61
 
    this.cursor = this.items.length;
 
164
    /* Copy the selected item's "edited" version over the permanent version of
 
165
     * the last item. */
 
166
    this.items[this.items.length-1] = text;
 
167
    /* Add a new blank item */
 
168
    this.items[this.items.length] = "";
 
169
    this.cursor = this.items.length-1;
 
170
    /* Blow away all the edited versions, replacing them with the existing
 
171
     * items set.
 
172
     * Not the whole history - just start from the earliest edited one.
 
173
     * (This avoids slowdown over extended usage time).
 
174
     */
 
175
    for (var i=this.earliestCursor; i<=this.cursor; i++)
 
176
        this.edited[i] = this.items[i];
 
177
    this.earliestCursor = this.cursor;
62
178
}
63
179
 
64
180
function historyShow()
65
181
{
66
182
    var res = "";
67
 
    if (this.cursor == -1)
68
 
    {
69
 
        res += "[]";
70
 
    }
71
183
    for (var i = 0; i < this.items.length; i++)
72
184
    {
73
185
        if (i == this.cursor)
88
200
    return res;
89
201
}
90
202
 
 
203
/* How history works
 
204
 * This is a fairly complex mechanism due to complications when editing
 
205
 * history items. We store two arrays. "items" is the permanent history of
 
206
 * each item. "edited" is a "volatile" version of items - the edits made to
 
207
 * the history between now and last time you hit "enter".
 
208
 * This is because the user can go back and edit any of the previous items,
 
209
 * and the edits are remembered until they hit enter.
 
210
 *
 
211
 * When hitting enter, the "edited" version of the currently selected item
 
212
 * replaces the "item" version of the last item in the list.
 
213
 * Then a new blank item is created, for the new line of input.
 
214
 * Lastly, all the "edited" versions are replaced with their stable versions.
 
215
 *
 
216
 * Cursor never points to an invalid location.
 
217
 */
91
218
function History()
92
219
{
93
 
    this.items = new Array();
94
 
    this.cursor = -1;
 
220
    this.items = new Array("");
 
221
    this.edited = new Array("");
 
222
    this.cursor = 0;
 
223
    this.earliestCursor = 0;
95
224
    this.up = historyUp;
96
225
    this.down = historyDown;
97
226
    this.curr = historyCurr;
98
 
    this.add = historyAdd;
 
227
    this.submit = historySubmit;
99
228
    this.show = historyShow;
100
229
}
101
230
 
102
231
var hist = new History();
103
232
 
104
 
function enter_line()
105
 
{
106
 
    var inp = document.getElementById('inputText');
107
 
    var digest = hex_md5(inp.value + magic);
108
 
    var args = {"host": server_host, "port": server_port,
109
 
                    "digest":digest, "text":inp.value};
110
 
    var xmlhttp = ajax_call("consoleservice", "chat", args, "POST");
111
 
 
112
 
    var res = JSON.parse(xmlhttp.responseText);
113
 
    var output = document.getElementById("output");
114
 
    {
115
 
        var pre = document.createElement("pre");
116
 
        pre.setAttribute("class", "inputMsg");
117
 
        pre.appendChild(document.createTextNode(inp.value + "\n"));
118
 
        output.appendChild(pre);
119
 
    }
 
233
function set_interrupt()
 
234
{
 
235
    interrupted = true;
 
236
}
 
237
 
 
238
function clear_output()
 
239
{
 
240
    var output = document.getElementById("console_output");
 
241
    while (output.firstChild)
 
242
    {
 
243
        output.removeChild(output.firstChild);
 
244
    }
 
245
}
 
246
 
 
247
/** Send a line of text to the Python server, wait for its return, and react
 
248
 * to its response by writing to the output box.
 
249
 * Also maximize the console window if not already.
 
250
 */
 
251
function console_enter_line(inputbox, which)
 
252
{
 
253
    interrupted = false;
 
254
 
 
255
    if (typeof(inputbox) == "string")
 
256
    {
 
257
        var inputline = inputbox;
 
258
        inputbox = null;
 
259
        var graytimer = null;
 
260
    }
 
261
    else
 
262
    {
 
263
        GLOBAL_inputbox = inputbox;     /* For timer */
 
264
        var inputline = inputbox.value;
 
265
        var graytimer = setTimeout("GLOBAL_inputbox.setAttribute(\"class\", "
 
266
            + "\"disabled\");", 100);
 
267
    }
 
268
    var output = document.getElementById("console_output");
 
269
    {
 
270
        // Print ">>>" span
 
271
        var span = document.createElement("span");
 
272
        span.setAttribute("class", "inputPrompt");
 
273
        span.appendChild(document.createTextNode(">>> "));
 
274
        output.appendChild(span);
 
275
        // Print input line itself in a span
 
276
        var span = document.createElement("span");
 
277
        span.setAttribute("class", "inputMsg");
 
278
        span.appendChild(document.createTextNode(inputline + "\n"));
 
279
        output.appendChild(span);
 
280
    }
 
281
    var args = {"key": server_key, "text":inputline};
 
282
    var callback = function(xhr)
 
283
        {
 
284
            console_response(inputbox, graytimer, inputline, xhr.responseText);
 
285
        }
 
286
    /* Disable the text box */
 
287
    if (inputbox != null)
 
288
        inputbox.setAttribute("disabled", "disabled");
 
289
    ajax_call(callback, "consoleservice", which, args, "POST");
 
290
}
 
291
 
 
292
function console_response(inputbox, graytimer, inputline, responseText)
 
293
{
 
294
    try
 
295
    {
 
296
        var res = JSON.parse(responseText);
 
297
    }
 
298
    catch (e)
 
299
    {
 
300
        alert("An internal error occurred in the python console.");
 
301
        return;
 
302
    }
 
303
    var output = document.getElementById("console_output");
120
304
    if (res.hasOwnProperty('okay'))
121
305
    {
122
 
        // Success!
123
 
        // print out the output (res.okay[0])
124
 
        var pre = document.createElement("pre");
125
 
        pre.setAttribute("class", "outputMsg");
126
 
        pre.appendChild(document.createTextNode(res.okay[0]));
127
 
        output.appendChild(pre);
128
 
        // print out the return value (res.okay[1])
129
 
        if (res.okay[1])
130
 
        {
131
 
            var pre = document.createElement("pre");
132
 
            pre.setAttribute("class", "outputMsg");
133
 
            pre.appendChild(document.createTextNode(res.okay[1] + "\n"));
134
 
            output.appendChild(pre);
135
 
        }
136
306
        // set the prompt to >>>
137
 
        var prompt = document.getElementById("prompt");
 
307
        var prompt = document.getElementById("console_prompt");
138
308
        prompt.replaceChild(document.createTextNode(">>> "), prompt.firstChild);
139
309
    }
140
310
    else if (res.hasOwnProperty('exc'))
141
311
    {
142
312
        // Failure!
143
313
        // print out the error message (res.exc)
144
 
        var pre = document.createElement("pre");
145
 
        pre.setAttribute("class", "errorMsg");
146
 
        pre.appendChild(document.createTextNode(res.exc));
147
 
        output.appendChild(pre);
 
314
        var span = document.createElement("span");
 
315
        span.setAttribute("class", "errorMsg");
 
316
        span.appendChild(document.createTextNode(res.exc + "\n"));
 
317
        output.appendChild(span);
 
318
        // set the prompt to >>>
 
319
        var prompt = document.getElementById("console_prompt");
 
320
        prompt.replaceChild(document.createTextNode(">>> "), prompt.firstChild);
 
321
    }
 
322
    else if (res.hasOwnProperty('restart') && res.hasOwnProperty('key'))
 
323
    {
 
324
        // Server has indicated that the console should be restarted
 
325
        
 
326
        // Get the new key (host, port, magic)
 
327
        server_key = res.key;
 
328
 
 
329
        // Print a reason to explain why we'd do such a horrible thing
 
330
        // (console timeout, server error etc.)
 
331
        var span = document.createElement("span");
 
332
        span.setAttribute("class", "errorMsg");
 
333
        span.appendChild(document.createTextNode("Console Restart: " + res.restart + "\n"));
 
334
        output.appendChild(span);
 
335
        // set the prompt to >>>
 
336
        var prompt = document.getElementById("console_prompt");
 
337
        prompt.replaceChild(document.createTextNode(">>> "), prompt.firstChild);
 
338
 
148
339
    }
149
340
    else if (res.hasOwnProperty('more'))
150
341
    {
151
342
        // Need more input, so set the prompt to ...
152
 
        var prompt = document.getElementById("prompt");
 
343
        var prompt = document.getElementById("console_prompt");
153
344
        prompt.replaceChild(document.createTextNode("... "), prompt.firstChild);
154
345
    }
 
346
    else if (res.hasOwnProperty('output'))
 
347
    {
 
348
        if (res.output.length > 0)
 
349
        {
 
350
            output.appendChild(document.createTextNode(res.output));
 
351
        }
 
352
        var callback = function(xhr)
 
353
            {
 
354
                console_response(inputbox, graytimer,
 
355
                                 null, xhr.responseText);
 
356
            }
 
357
        if (interrupted)
 
358
        {
 
359
            var kind = "interrupt";
 
360
        }
 
361
        else
 
362
        {
 
363
            var kind = "chat";
 
364
        }
 
365
        var args = {"key": server_key, "text":''};
 
366
        ajax_call(callback, "consoleservice", kind, args, "POST");
 
367
 
 
368
        // Open up the console so we can see the output
 
369
        // FIXME: do we need to maximize here?
 
370
        console_maximize();
 
371
 
 
372
        /* Auto-scrolling */
 
373
        divScroll.activeScroll();
 
374
 
 
375
        // Return early, so we don't re-enable the input box.
 
376
        return;
 
377
    }
155
378
    else {
156
379
        // assert res.hasOwnProperty('input')
157
 
        var prompt = document.getElementById("prompt");
 
380
        var prompt = document.getElementById("console_prompt");
158
381
        prompt.replaceChild(document.createTextNode("+++ "), prompt.firstChild);
159
382
    }
 
383
 
 
384
    if (inputbox != null)
 
385
    {
 
386
        /* Re-enable the text box */
 
387
        clearTimeout(graytimer);
 
388
        inputbox.removeAttribute("disabled");
 
389
        inputbox.removeAttribute("class");
 
390
        interrupted = false;
 
391
    }
 
392
 
 
393
    /* Open up the console so we can see the output */
 
394
    console_maximize();
 
395
    /* Auto-scrolling */
 
396
    divScroll.activeScroll();
 
397
 
 
398
    // Focus the input box by default
 
399
    document.getElementById("console_output").focus()
 
400
    document.getElementById("console_inputText").focus()
160
401
}
161
402
 
162
403
function catch_input(key)
163
404
{
164
 
    var inp = document.getElementById('inputText');
165
 
    if (key == 13)
166
 
    {
167
 
        enter_line();
168
 
        hist.add(inp.value);
169
 
        inp.value = hist.curr();
170
 
    }
171
 
    if (key == 38)
172
 
    {
173
 
        hist.up();
174
 
        inp.value = hist.curr();
175
 
    }
176
 
    if (key == 40)
177
 
    {
178
 
        hist.down();
179
 
        inp.value = hist.curr();
180
 
    }
181
 
}
 
405
    var inp = document.getElementById('console_inputText');
 
406
    switch (key)
 
407
    {
 
408
    case 9:                 /* Tab key */
 
409
        var selstart = inp.selectionStart;
 
410
        var selend = inp.selectionEnd;
 
411
        if (selstart == selend)
 
412
        {
 
413
            /* No selection, just a carat. Insert a tab here. */
 
414
            inp.value = inp.value.substr(0, selstart)
 
415
                + TAB_STRING + inp.value.substr(selstart);
 
416
        }
 
417
        else
 
418
        {
 
419
            /* Text is selected. Just indent the whole line
 
420
             * by inserting a tab at the start */
 
421
            inp.value = TAB_STRING + inp.value;
 
422
        }
 
423
        /* Update the selection so the same characters as before are selected
 
424
         */
 
425
        inp.selectionStart = selstart + TAB_STRING.length;
 
426
        inp.selectionEnd = inp.selectionStart + (selend - selstart);
 
427
        /* Cancel the event, so the TAB key doesn't move focus away from this
 
428
         * box */
 
429
        return false;
 
430
        /* Note: If it happens that some browsers don't support event
 
431
         * cancelling properly, this hack might work instead:
 
432
        setTimeout(
 
433
            "document.getElementById('console_inputText').focus()",
 
434
            0);
 
435
         */
 
436
        break;
 
437
    case 13:                /* Enter key */
 
438
        var callback = function()
 
439
        {
 
440
            /* Send the line of text to the server */
 
441
            console_enter_line(inp, "chat");
 
442
            hist.submit(inp.value);
 
443
            inp.value = hist.curr();
 
444
        }
 
445
        /* Start the server if it hasn't already been started */
 
446
        start_server(callback);
 
447
        break;
 
448
    case 38:                /* Up arrow */
 
449
        hist.up(inp.value);
 
450
        inp.value = hist.curr();
 
451
        break;
 
452
    case 40:                /* Down arrow */
 
453
        hist.down(inp.value);
 
454
        inp.value = hist.curr();
 
455
        break;
 
456
    }
 
457
}
 
458
 
 
459
/**** Following Code modified from ******************************************/
 
460
/**** http://radio.javaranch.com/pascarello/2006/08/17/1155837038219.html ***/
 
461
/****************************************************************************/
 
462
var chatscroll = new Object();
 
463
 
 
464
chatscroll.Pane = function(scrollContainerId)
 
465
{
 
466
    this.scrollContainerId = scrollContainerId;
 
467
}
 
468
 
 
469
chatscroll.Pane.prototype.activeScroll = function()
 
470
{
 
471
    var scrollDiv = document.getElementById(this.scrollContainerId);
 
472
    var currentHeight = 0;
 
473
        
 
474
    if (scrollDiv.scrollHeight > 0)
 
475
        currentHeight = scrollDiv.scrollHeight;
 
476
    else 
 
477
        if (objDiv.offsetHeight > 0)
 
478
            currentHeight = scrollDiv.offsetHeight;
 
479
 
 
480
    scrollDiv.scrollTop = currentHeight;
 
481
 
 
482
    scrollDiv = null;
 
483
}
 
484
 
 
485
var divScroll = new chatscroll.Pane('console_output');