~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:54:34 UTC
  • Revision ID: svn-v3-trunk0:2b9c9e99-6f39-0410-b283-7f802c844ae2:trunk:629
console: a couple of minor tweaks arising from conversation with Adrian.

Show diffs side-by-side

added added

removed removed

Lines of Context:
109
109
    if (!windowpane_mode) return;
110
110
    console_body.setAttribute("class", "windowpane maximal");
111
111
    console_filler.setAttribute("class", "windowpane maximal");
112
 
    /* Focus the input box by default */
113
 
    document.getElementById("console_inputText").focus()
114
112
}
115
113
 
116
114
/* current_text is the string currently on the command line.
319
317
        var args = {"key": server_key, "text":''};
320
318
        ajax_call(callback, "consoleservice", kind, args, "POST");
321
319
 
322
 
        /* Open up the console so we can see the output */
 
320
        // Open up the console so we can see the output
 
321
        // FIXME: do we need to maximize here?
323
322
        console_maximize();
 
323
 
324
324
        /* Auto-scrolling */
325
325
        divScroll.activeScroll();
326
326
 
346
346
    console_maximize();
347
347
    /* Auto-scrolling */
348
348
    divScroll.activeScroll();
 
349
 
 
350
    // Focus the input box by default
 
351
    // document.getElementById("console_inputText").focus()
349
352
}
350
353
 
351
354
function catch_input(key)