← 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: drtomc
  • Date: 2008-02-29 03:00:36 UTC
  • Revision ID: svn-v3-trunk0:2b9c9e99-6f39-0410-b283-7f802c844ae2:trunk:628
console: Add output based interrupt. This allows users to interrupt long
         running outputs.
         TODO: poll for interrupts from cpu intensive ops.
         TODO: styling bug: the input box overlaps the output box. Matt?

Show diffs side-by-side

added added

removed removed

Lines of Context:
www/media/console/console.js
34
34
windowpane_mode = false;
35
35
server_started = false;
36
36
 
 
37
interrupted = false;
 
38
 
37
39
/* Starts the console server, if it isn't already.
38
40
 * This can be called any number of times - it only starts the one server.
39
41
 * Note that this is asynchronous. It will return after signalling to start
211
213
 
212
214
var hist = new History();
213
215
 
 
216
function set_interrupt()
 
217
{
 
218
    interrupted = true;
 
219
}
 
220
 
 
221
function clear_output()
 
222
{
 
223
    var output = document.getElementById("console_output");
 
224
    while (output.firstChild)
 
225
    {
 
226
        output.removeChild(output.firstChild);
 
227
    }
 
228
}
 
229
 
214
230
/** Send a line of text to the Python server, wait for its return, and react
215
231
 * to its response by writing to the output box.
216
232
 * Also maximize the console window if not already.
217
233
 */
218
234
function console_enter_line(inputbox, which)
219
235
{
 
236
    interrupted = false;
 
237
 
220
238
    if (typeof(inputbox) == "string")
221
239
    {
222
240
        var inputline = inputbox;
290
308
                console_response(inputbox, graytimer,
291
309
                                 null, xhr.responseText);
292
310
            }
 
311
        if (interrupted)
 
312
        {
 
313
            var kind = "interrupt";
 
314
        }
 
315
        else
 
316
        {
 
317
            var kind = "chat";
 
318
        }
293
319
        var args = {"key": server_key, "text":''};
294
 
        ajax_call(callback, "consoleservice", "chat", args, "POST");
 
320
        ajax_call(callback, "consoleservice", kind, args, "POST");
295
321
 
296
322
        /* Open up the console so we can see the output */
297
323
        console_maximize();
313
339
        clearTimeout(graytimer);
314
340
        inputbox.removeAttribute("disabled");
315
341
        inputbox.removeAttribute("class");
 
342
        interrupted = false;
316
343
    }
317
344
 
318
345
    /* Open up the console so we can see the output */