~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-02-05 01:41:15 UTC
  • Revision ID: svn-v3-trunk0:2b9c9e99-6f39-0410-b283-7f802c844ae2:trunk:409
Moved www/conf and www/common to a new directory lib. This separates the "web"
part of IVLE from what is becoming less web oriented (at least from Apache's
standpoint).
Modified setup.py to install this lib directory correctly and write conf in
the right place. Also adds the lib directory to ivle.pth.

Show diffs side-by-side

added added

removed removed

Lines of Context:
20
20
 * Date: 30/1/2008
21
21
 */
22
22
 
23
 
var server_key;
 
23
digest_constant = "hello";
 
24
 
 
25
var server_host;
 
26
var server_port;
 
27
var server_magic;
24
28
 
25
29
/* Begin religious debate (tabs vs spaces) here: */
26
30
/* (This string will be inserted in the console when the user presses the Tab
34
38
windowpane_mode = false;
35
39
server_started = false;
36
40
 
37
 
interrupted = false;
38
 
 
39
41
/* Starts the console server, if it isn't already.
40
42
 * 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
43
 * This is a separate step from console_init, as the server is only to be
44
44
 * started once the first command is entered.
45
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.
 
46
 * server_host, server_port, server_magic.
50
47
 */
51
 
function start_server(callback)
 
48
function start_server()
52
49
{
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
 
    }
 
50
    if (server_started) return;
 
51
    var xhr = ajax_call("consoleservice", "start", {}, "POST");
 
52
    var json_text = xhr.responseText;
 
53
    var server_info = JSON.parse(json_text);
 
54
    server_host = server_info.host;
 
55
    server_port = server_info.port;
 
56
    server_magic = server_info.magic;
 
57
    server_started = true;
91
58
}
92
59
 
93
60
/** Initialises the console. All apps which import console are required to
110
77
        windowpane_mode = true;
111
78
        console_minimize();
112
79
    }
 
80
    /* TEMP: Start the server now.
 
81
     * Ultimately we want the server to start only when a line is typed, but
 
82
     * it currently does it asynchronously and doesn't start in time for the
 
83
     * first line. */
 
84
    start_server();
113
85
}
114
86
 
115
87
/** Hide the main console panel, so the console minimizes to just an input box
128
100
    if (!windowpane_mode) return;
129
101
    console_body.setAttribute("class", "windowpane maximal");
130
102
    console_filler.setAttribute("class", "windowpane maximal");
 
103
    /* Focus the input box by default */
 
104
    document.getElementById("console_inputText").focus()
131
105
}
132
106
 
133
107
/* current_text is the string currently on the command line.
230
204
 
231
205
var hist = new History();
232
206
 
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
207
/** Send a line of text to the Python server, wait for its return, and react
248
208
 * to its response by writing to the output box.
249
209
 * Also maximize the console window if not already.
250
210
 */
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");
 
211
function console_enter_line(inputline, which)
 
212
{
 
213
    /* Start the server if it hasn't already been started */
 
214
    start_server();
 
215
    var digest = hex_md5(inputline + server_magic);
 
216
    var args = {"host": server_host, "port": server_port,
 
217
                    "digest":digest, "text":inputline};
 
218
    var xmlhttp = ajax_call("consoleservice", which, args, "POST");
 
219
 
 
220
    var res = JSON.parse(xmlhttp.responseText);
 
221
    var output = document.getElementById("console_output");
 
222
    {
 
223
        var pre = document.createElement("pre");
 
224
        pre.setAttribute("class", "inputMsg");
 
225
        pre.appendChild(document.createTextNode(inputline + "\n"));
 
226
        output.appendChild(pre);
 
227
    }
304
228
    if (res.hasOwnProperty('okay'))
305
229
    {
 
230
        // Success!
 
231
        // print out the output (res.okay[0])
 
232
        var pre = document.createElement("pre");
 
233
        pre.setAttribute("class", "outputMsg");
 
234
        pre.appendChild(document.createTextNode(res.okay[0]));
 
235
        output.appendChild(pre);
 
236
        // print out the return value (res.okay[1])
 
237
        if (res.okay[1])
 
238
        {
 
239
            var pre = document.createElement("pre");
 
240
            pre.setAttribute("class", "outputMsg");
 
241
            pre.appendChild(document.createTextNode(res.okay[1] + "\n"));
 
242
            output.appendChild(pre);
 
243
        }
306
244
        // set the prompt to >>>
307
245
        var prompt = document.getElementById("console_prompt");
308
246
        prompt.replaceChild(document.createTextNode(">>> "), prompt.firstChild);
310
248
    else if (res.hasOwnProperty('exc'))
311
249
    {
312
250
        // Failure!
 
251
        // print out any output that came before the error
 
252
        if (res.exc[0].length > 0)
 
253
        {
 
254
            var pre = document.createElement("pre");
 
255
            pre.setAttribute("class", "outputMsg");
 
256
            pre.appendChild(document.createTextNode(res.exc[0]));
 
257
            output.appendChild(pre);
 
258
        }
 
259
 
313
260
        // print out the error message (res.exc)
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
 
 
 
261
        var pre = document.createElement("pre");
 
262
        pre.setAttribute("class", "errorMsg");
 
263
        pre.appendChild(document.createTextNode(res.exc[1]));
 
264
        output.appendChild(pre);
339
265
    }
340
266
    else if (res.hasOwnProperty('more'))
341
267
    {
343
269
        var prompt = document.getElementById("console_prompt");
344
270
        prompt.replaceChild(document.createTextNode("... "), prompt.firstChild);
345
271
    }
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
 
    }
378
272
    else {
379
273
        // assert res.hasOwnProperty('input')
380
274
        var prompt = document.getElementById("console_prompt");
381
275
        prompt.replaceChild(document.createTextNode("+++ "), prompt.firstChild);
382
276
    }
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
277
    /* Open up the console so we can see the output */
394
278
    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()
401
279
}
402
280
 
403
281
function catch_input(key)
435
313
         */
436
314
        break;
437
315
    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);
 
316
        /* Send the line of text to the server */
 
317
        console_enter_line(inp.value, "chat");
 
318
        hist.submit(inp.value);
 
319
        inp.value = hist.curr();
447
320
        break;
448
321
    case 38:                /* Up arrow */
449
322
        hist.up(inp.value);
455
328
        break;
456
329
    }
457
330
}
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');