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

« back to all changes in this revision

Viewing changes to ivle/webapp/console/media/console.js

  • Committer: David Coles
  • Date: 2010-07-16 06:47:19 UTC
  • Revision ID: coles.david@gmail.com-20100716064719-j68ejmcf6akblw8a
Fix typo in rebuild_svn_config that caused Storm query to return limited or no 
submissions.

Fixes issue where lectueres and tutors did not have permission to access 
submissions by students in their subjects.

Show diffs side-by-side

added added

removed removed

Lines of Context:
36
36
 
37
37
interrupted = false;
38
38
 
 
39
 
 
40
function get_console_start_directory()
 
41
{
 
42
    if((typeof(current_path) != 'undefined') && current_file)
 
43
    {
 
44
        // We have a current_path - give a suggestion to the server
 
45
        var path;
 
46
        if (current_file.isdir)
 
47
        {
 
48
            // Browser
 
49
            return path_join("/home", current_path);
 
50
        }
 
51
        else
 
52
        {
 
53
            // Editor - need to chop off filename
 
54
            var tmp_path = current_path.split('/');
 
55
            tmp_path.pop();
 
56
            return path_join("/home", tmp_path.join('/'));
 
57
        }
 
58
    }
 
59
    else
 
60
    {
 
61
        // No current_path - let the server decide
 
62
        return '';
 
63
    }
 
64
}
 
65
 
39
66
/* Starts the console server, if it isn't already.
40
67
 * This can be called any number of times - it only starts the one server.
41
68
 * Note that this is asynchronous. It will return after signalling to start
58
85
    var callback1 = function(xhr)
59
86
        {
60
87
            var json_text = xhr.responseText;
61
 
            server_key = JSON.parse(json_text).key;
62
 
            server_started = true;
63
 
            if (callback != null)
64
 
                callback();
65
 
        }
66
 
 
67
 
    //var current_path;
68
 
    if((typeof(current_path) != 'undefined') && current_file)
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, "console", "service", {"ivle.op": "start", "cwd": path}, "POST");
85
 
    }
86
 
    else
87
 
    {
88
 
        // No current_path - let the server decide
89
 
        ajax_call(callback1, "console", "service", {"ivle.op": "start"}, "POST");
90
 
    }
 
88
            try
 
89
            {
 
90
                server_key = JSON.parse(json_text).key;
 
91
                server_started = true;
 
92
                var args = {
 
93
                    "ivle.op": "chat", "kind": "splash", "key": server_key
 
94
                };
 
95
                var callback2 = function(xhr)
 
96
                {
 
97
                    console_response(null, null, xhr.responseText);
 
98
                    if (callback != null)
 
99
                        callback();
 
100
                };
 
101
                ajax_call(callback2, "console", "service", args, "POST");
 
102
            }
 
103
            catch (e)
 
104
            {
 
105
                alert("An error occured when starting the IVLE console. " +
 
106
                    "Please refresh the page and try again.\n" +
 
107
                    "Details have been logged for further examination.")
 
108
            }
 
109
        }
 
110
 
 
111
    $("#console_output").append(
 
112
        '<span class="console_message">IVLE console starting up...</span>\n');
 
113
    console_maximize(true);
 
114
    ajax_call(
 
115
        callback1, "console", "service",
 
116
        {"ivle.op": "start", "cwd": get_console_start_directory()}, 
 
117
        "POST");
 
118
}
 
119
 
 
120
/** Start up the console backend before the user has entered text.
 
121
 * This will disable the text input, start a backend, and enable the input
 
122
 * again.
 
123
 */
 
124
function start_server_early()
 
125
{
 
126
    var inputbox = document.getElementById("console_inputText");
 
127
    inputbox.setAttribute("disabled", "disabled");
 
128
    var callback = function(xhr)
 
129
    {
 
130
        inputbox.removeAttribute("disabled")
 
131
    }
 
132
    start_server(callback);
91
133
}
92
134
 
93
135
/** Initialises the console. All apps which import console are required to
117
159
function console_minimize()
118
160
{
119
161
    if (!windowpane_mode) return;
120
 
    console_body.setAttribute("class", "windowpane minimal");
 
162
    console_body.setAttribute("class", "console_body windowpane minimal");
121
163
    console_filler.setAttribute("class", "windowpane minimal");
122
164
}
123
165
 
124
166
/** Show the main console panel, so it enlarges out to its full size.
125
167
 */
126
 
function console_maximize()
 
168
function console_maximize(do_not_start)
127
169
{
128
170
    if (!windowpane_mode) return;
129
 
    console_body.setAttribute("class", "windowpane maximal");
 
171
    if (!do_not_start && !server_started) start_server_early();
 
172
    console_body.setAttribute("class", "console_body windowpane maximal");
130
173
    console_filler.setAttribute("class", "windowpane maximal");
131
174
}
132
175
 
252
295
{
253
296
    interrupted = false;
254
297
 
 
298
    // Open up the console so we can see the output
 
299
    console_maximize();
 
300
 
255
301
    if (typeof(inputbox) == "string")
256
302
    {
257
 
        var inputline = inputbox;
 
303
        var inputline = inputbox + "\n";
258
304
        inputbox = null;
259
 
        var graytimer = null;
260
305
    }
261
306
    else
262
307
    {
263
 
        GLOBAL_inputbox = inputbox;     /* For timer */
 
308
        /* Disable the text box */
 
309
        inputbox.setAttribute("disabled", "disabled");
 
310
 
264
311
        var inputline = inputbox.value + "\n";
265
 
        var graytimer = setTimeout("GLOBAL_inputbox.setAttribute(\"class\", "
266
 
            + "\"disabled\");", 100);
267
312
    }
268
313
    var output = document.getElementById("console_output");
269
314
    {
271
316
        var span = document.createElement("span");
272
317
        span.setAttribute("class", "inputPrompt");
273
318
        span.appendChild(document.createTextNode(
274
 
              document.getElementById("console_prompt").firstChild.textContent)
 
319
              document.getElementById("console_prompt").firstChild.nodeValue)
275
320
                        );
276
321
        output.appendChild(span);
277
322
        // Print input line itself in a span
279
324
        span.setAttribute("class", "inputMsg");
280
325
        span.appendChild(document.createTextNode(inputline));
281
326
        output.appendChild(span);
 
327
        divScroll.activeScroll();
282
328
    }
283
 
    var args = {"ivle.op": "chat", "kind": which, "key": server_key, "text":inputline};
 
329
    var args = {
 
330
        "ivle.op": "chat", "kind": which, "key": server_key,
 
331
        "text": inputline, "cwd": get_console_start_directory()
 
332
        };
284
333
    var callback = function(xhr)
285
334
        {
286
 
            console_response(inputbox, graytimer, inputline, xhr.responseText);
 
335
            console_response(inputbox, inputline, xhr.responseText);
287
336
        }
288
 
    /* Disable the text box */
289
 
    if (inputbox != null)
290
 
        inputbox.setAttribute("disabled", "disabled");
291
337
    ajax_call(callback, "console", "service", args, "POST");
292
338
}
293
339
 
294
 
function console_response(inputbox, graytimer, inputline, responseText)
 
340
function console_response(inputbox, inputline, responseText)
295
341
{
296
342
    try
297
343
    {
310
356
        {
311
357
            output.appendChild(document.createTextNode(res.okay + "\n"));
312
358
            output.appendChild(span);
 
359
            divScroll.activeScroll();
313
360
        }
314
361
        // set the prompt to >>>
315
362
        set_prompt(">>>");
332
379
 
333
380
        // Print a reason to explain why we'd do such a horrible thing
334
381
        // (console timeout, server error etc.)
335
 
        print_error("Console Restart: " + res.restart);
 
382
        print_error(
 
383
            "IVLE console restarted: " + res.restart, "console_message");
336
384
        
337
385
        // set the prompt to >>>
338
386
        set_prompt(">>>");
347
395
        if (res.output.length > 0)
348
396
        {
349
397
            output.appendChild(document.createTextNode(res.output));
 
398
            divScroll.activeScroll();
350
399
        }
351
400
        var callback = function(xhr)
352
401
            {
353
 
                console_response(inputbox, graytimer,
354
 
                                 null, xhr.responseText);
 
402
                console_response(inputbox, null, xhr.responseText);
355
403
            }
356
404
        if (interrupted)
357
405
        {
361
409
        {
362
410
            var kind = "chat";
363
411
        }
364
 
        var args = {"ivle.op": "chat", "kind": kind, "key": server_key, "text":''};
 
412
        var args = {
 
413
            "ivle.op": "chat", "kind": kind, "key": server_key,
 
414
            "text": '', "cwd": get_console_start_directory()
 
415
            };
365
416
        ajax_call(callback, "console", "service", args, "POST");
366
417
 
367
418
        // Open up the console so we can see the output
368
 
        // FIXME: do we need to maximize here?
369
419
        console_maximize();
370
420
 
371
 
        /* Auto-scrolling */
372
 
        divScroll.activeScroll();
373
 
 
374
421
        // Return early, so we don't re-enable the input box.
375
422
        return;
376
423
    }
 
424
    else if (res.hasOwnProperty('input'))
 
425
    {
 
426
        set_prompt("+++");
 
427
    }
377
428
    else
378
429
    {
379
 
        // assert res.hasOwnProperty('input')
380
 
        set_prompt("...");
 
430
        alert("An internal error occurred in the python console.");
 
431
        return;
381
432
    }
382
433
 
383
434
    if (inputbox != null)
384
435
    {
385
436
        /* Re-enable the text box */
386
 
        clearTimeout(graytimer);
387
437
        inputbox.removeAttribute("disabled");
388
 
        inputbox.removeAttribute("class");
389
438
        interrupted = false;
390
439
    }
391
440
 
392
 
    /* Open up the console so we can see the output */
393
 
    console_maximize();
394
441
    /* Auto-scrolling */
395
442
    divScroll.activeScroll();
396
443
 
441
488
            hist.submit(inp.value);
442
489
            inp.value = hist.curr();
443
490
        }
 
491
 
 
492
        /* Disable the text box. This will be redone by
 
493
         * console_enter_line, but we do it here too in case start_server
 
494
         * takes a while.
 
495
         */
 
496
        inp.setAttribute("disabled", "disabled");
444
497
        /* Start the server if it hasn't already been started */
445
498
        start_server(callback);
446
499
        break;
447
500
    case 38:                /* Up arrow */
448
501
        hist.up(inp.value);
449
502
        inp.value = hist.curr();
 
503
        /* Inhibit further responses to this event, or WebKit moves the
 
504
         * cursor to the start. */
 
505
        return false;
450
506
        break;
451
507
    case 40:                /* Down arrow */
452
508
        hist.down(inp.value);
453
509
        inp.value = hist.curr();
 
510
        return false;
454
511
        break;
455
512
    }
456
513
}
470
527
    }
471
528
    else
472
529
    {
473
 
        xhr = ajax_call(null, "console", "service", {"ivle.op": "chat", "kind": "terminate", "key": server_key}, "POST");
474
 
        console_response(null, null, null, xhr.responseText);
 
530
        xhr = ajax_call(null, "console", "service", {"ivle.op": "chat", "kind": "terminate", "key": server_key, "cwd": get_console_start_directory()}, "POST");
 
531
        console_response(null, null, xhr.responseText);
475
532
    }
476
533
}
477
534
 
478
535
/** Prints an error line in the console **/
479
 
function print_error(error)
480
 
 
536
function print_error(error, cls)
 
537
{
 
538
    if (!cls)
 
539
        cls = "errorMsg";
 
540
 
481
541
    var output = document.getElementById("console_output");
482
542
  
483
543
    // Create text block
484
544
    var span = document.createElement("span");
485
 
    span.setAttribute("class", "errorMsg");
 
545
    span.setAttribute("class", cls);
486
546
    span.appendChild(document.createTextNode(error + "\n"));
487
547
    output.appendChild(span);
488
548