← 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-04-16 16:11:49 UTC
  • Revision ID: svn-v3-trunk0:2b9c9e99-6f39-0410-b283-7f802c844ae2:trunk:733
db.py: Added new function set_worksheet_assessable.
    Realised that if create_worksheet was used to update assessable, then
    mtime would be set to the current time, and therefore when you go to
    update based on the worksheet.xml, it will look like it's already
    up-to-date. BAD!!

    Therefore, you use set_worksheet_assessable to update the "assessable"
    field without setting the new mtime.

Show diffs side-by-side

added added

removed removed

Lines of Context:
www/media/console/console.js
 
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
    ajax_call(callback1, "consoleservice", "start", {}, "POST");
 
67
}
 
68
 
 
69
/** Initialises the console. All apps which import console are required to
 
70
 * call this function.
 
71
 * Optional "windowpane" (bool), if true, will cause the console to go into
 
72
 * "window pane" mode which will allow it to be opened and closed, and float
 
73
 * over the page.
 
74
 * (Defaults to closed).
 
75
 */
 
76
function console_init(windowpane)
 
77
{
 
78
    /* Set up the console as a floating pane */
 
79
    console_body = document.getElementById("console_body");
 
80
    /* If there is no console body, don't worry.
 
81
     * (This lets us import console.js even on pages without a console box */
 
82
    if (console_body == null) return;
 
83
    console_filler = document.getElementById("console_filler");
 
84
    if (windowpane)
 
85
    {
 
86
        windowpane_mode = true;
 
87
        console_minimize();
 
88
    }
 
89
}
 
90
 
 
91
/** Hide the main console panel, so the console minimizes to just an input box
 
92
 *  at the page bottom. */
 
93
function console_minimize()
 
94
{
 
95
    if (!windowpane_mode) return;
 
96
    console_body.setAttribute("class", "windowpane minimal");
 
97
    console_filler.setAttribute("class", "windowpane minimal");
 
98
}
 
99
 
 
100
/** Show the main console panel, so it enlarges out to its full size.
 
101
 */
 
102
function console_maximize()
 
103
{
 
104
    if (!windowpane_mode) return;
 
105
    console_body.setAttribute("class", "windowpane maximal");
 
106
    console_filler.setAttribute("class", "windowpane maximal");
 
107
}
 
108
 
 
109
/* current_text is the string currently on the command line.
 
110
 * If non-empty, it will be stored at the bottom of the history.
 
111
 */
 
112
function historyUp(current_text)
 
113
{
 
114
    /* Remember the changes made to this item */
 
115
    this.edited[this.cursor] = current_text;
 
116
    if (this.cursor > 0)
 
117
    {
 
118
        this.cursor--;
 
119
    }
 
120
    this.earliestCursor = this.cursor;
 
121
}
 
122
 
 
123
function historyDown(current_text)
 
124
{
 
125
    /* Remember the changes made to this item */
 
126
    this.edited[this.cursor] = current_text;
 
127
    if (this.cursor < this.items.length - 1)
 
128
    {
 
129
        this.cursor++;
 
130
    }
 
131
}
 
132
 
 
133
function historyCurr()
 
134
{
 
135
    return this.edited[this.cursor];
 
136
}
 
137
 
 
138
function historySubmit(text)
 
139
{
 
140
    /* Copy the selected item's "edited" version over the permanent version of
 
141
     * the last item. */
 
142
    this.items[this.items.length-1] = text;
 
143
    /* Add a new blank item */
 
144
    this.items[this.items.length] = "";
 
145
    this.cursor = this.items.length-1;
 
146
    /* Blow away all the edited versions, replacing them with the existing
 
147
     * items set.
 
148
     * Not the whole history - just start from the earliest edited one.
 
149
     * (This avoids slowdown over extended usage time).
 
150
     */
 
151
    for (var i=this.earliestCursor; i<=this.cursor; i++)
 
152
        this.edited[i] = this.items[i];
 
153
    this.earliestCursor = this.cursor;
 
154
}
 
155
 
 
156
function historyShow()
 
157
{
 
158
    var res = "";
 
159
    for (var i = 0; i < this.items.length; i++)
 
160
    {
 
161
        if (i == this.cursor)
 
162
        {
 
163
            res += "["
 
164
        }
 
165
        res += this.items[i].toString();
 
166
        if (i == this.cursor)
 
167
        {
 
168
            res += "]"
 
169
        }
 
170
        res += " "
 
171
    }
 
172
    if (this.cursor == this.items.length)
 
173
    {
 
174
        res += "[]";
 
175
    }
 
176
    return res;
 
177
}
 
178
 
 
179
/* How history works
 
180
 * This is a fairly complex mechanism due to complications when editing
 
181
 * history items. We store two arrays. "items" is the permanent history of
 
182
 * each item. "edited" is a "volatile" version of items - the edits made to
 
183
 * the history between now and last time you hit "enter".
 
184
 * This is because the user can go back and edit any of the previous items,
 
185
 * and the edits are remembered until they hit enter.
 
186
 *
 
187
 * When hitting enter, the "edited" version of the currently selected item
 
188
 * replaces the "item" version of the last item in the list.
 
189
 * Then a new blank item is created, for the new line of input.
 
190
 * Lastly, all the "edited" versions are replaced with their stable versions.
 
191
 *
 
192
 * Cursor never points to an invalid location.
 
193
 */
 
194
function History()
 
195
{
 
196
    this.items = new Array("");
 
197
    this.edited = new Array("");
 
198
    this.cursor = 0;
 
199
    this.earliestCursor = 0;
 
200
    this.up = historyUp;
 
201
    this.down = historyDown;
 
202
    this.curr = historyCurr;
 
203
    this.submit = historySubmit;
 
204
    this.show = historyShow;
 
205
}
 
206
 
 
207
var hist = new History();
 
208
 
 
209
function set_interrupt()
 
210
{
 
211
    interrupted = true;
 
212
}
 
213
 
 
214
function clear_output()
 
215
{
 
216
    var output = document.getElementById("console_output");
 
217
    while (output.firstChild)
 
218
    {
 
219
        output.removeChild(output.firstChild);
 
220
    }
 
221
}
 
222
 
 
223
/** Send a line of text to the Python server, wait for its return, and react
 
224
 * to its response by writing to the output box.
 
225
 * Also maximize the console window if not already.
 
226
 */
 
227
function console_enter_line(inputbox, which)
 
228
{
 
229
    interrupted = false;
 
230
 
 
231
    if (typeof(inputbox) == "string")
 
232
    {
 
233
        var inputline = inputbox;
 
234
        inputbox = null;
 
235
        var graytimer = null;
 
236
    }
 
237
    else
 
238
    {
 
239
        GLOBAL_inputbox = inputbox;     /* For timer */
 
240
        var inputline = inputbox.value;
 
241
        var graytimer = setTimeout("GLOBAL_inputbox.setAttribute(\"class\", "
 
242
            + "\"disabled\");", 100);
 
243
    }
 
244
    var output = document.getElementById("console_output");
 
245
    {
 
246
        // Print ">>>" span
 
247
        var span = document.createElement("span");
 
248
        span.setAttribute("class", "inputPrompt");
 
249
        span.appendChild(document.createTextNode(">>> "));
 
250
        output.appendChild(span);
 
251
        // Print input line itself in a span
 
252
        var span = document.createElement("span");
 
253
        span.setAttribute("class", "inputMsg");
 
254
        span.appendChild(document.createTextNode(inputline + "\n"));
 
255
        output.appendChild(span);
 
256
    }
 
257
    var args = {"key": server_key, "text":inputline};
 
258
    var callback = function(xhr)
 
259
        {
 
260
            console_response(inputbox, graytimer, inputline, xhr.responseText);
 
261
        }
 
262
    /* Disable the text box */
 
263
    if (inputbox != null)
 
264
        inputbox.setAttribute("disabled", "disabled");
 
265
    ajax_call(callback, "consoleservice", which, args, "POST");
 
266
}
 
267
 
 
268
function console_response(inputbox, graytimer, inputline, responseText)
 
269
{
 
270
    try
 
271
    {
 
272
        var res = JSON.parse(responseText);
 
273
    }
 
274
    catch (e)
 
275
    {
 
276
        alert("An internal error occurred in the python console.");
 
277
        return;
 
278
    }
 
279
    var output = document.getElementById("console_output");
 
280
    if (res.hasOwnProperty('okay'))
 
281
    {
 
282
        // Success!
 
283
        if (res.okay)
 
284
        {
 
285
            output.appendChild(document.createTextNode(res.okay + "\n"));
 
286
            output.appendChild(span);
 
287
        }
 
288
        // set the prompt to >>>
 
289
        var prompt = document.getElementById("console_prompt");
 
290
        prompt.replaceChild(document.createTextNode(">>> "), prompt.firstChild);
 
291
    }
 
292
    else if (res.hasOwnProperty('exc'))
 
293
    {
 
294
        // Failure!
 
295
        // print out the error message (res.exc)
 
296
        var span = document.createElement("span");
 
297
        span.setAttribute("class", "errorMsg");
 
298
        span.appendChild(document.createTextNode(res.exc + "\n"));
 
299
        output.appendChild(span);
 
300
        // set the prompt to >>>
 
301
        var prompt = document.getElementById("console_prompt");
 
302
        prompt.replaceChild(document.createTextNode(">>> "), prompt.firstChild);
 
303
    }
 
304
    else if (res.hasOwnProperty('more'))
 
305
    {
 
306
        // Need more input, so set the prompt to ...
 
307
        var prompt = document.getElementById("console_prompt");
 
308
        prompt.replaceChild(document.createTextNode("... "), prompt.firstChild);
 
309
    }
 
310
    else if (res.hasOwnProperty('output'))
 
311
    {
 
312
        if (res.output.length > 0)
 
313
        {
 
314
            output.appendChild(document.createTextNode(res.output));
 
315
        }
 
316
        var callback = function(xhr)
 
317
            {
 
318
                console_response(inputbox, graytimer,
 
319
                                 null, xhr.responseText);
 
320
            }
 
321
        if (interrupted)
 
322
        {
 
323
            var kind = "interrupt";
 
324
        }
 
325
        else
 
326
        {
 
327
            var kind = "chat";
 
328
        }
 
329
        var args = {"key": server_key, "text":''};
 
330
        ajax_call(callback, "consoleservice", kind, args, "POST");
 
331
 
 
332
        // Open up the console so we can see the output
 
333
        // FIXME: do we need to maximize here?
 
334
        console_maximize();
 
335
 
 
336
        /* Auto-scrolling */
 
337
        divScroll.activeScroll();
 
338
 
 
339
        // Return early, so we don't re-enable the input box.
 
340
        return;
 
341
    }
 
342
    else {
 
343
        // assert res.hasOwnProperty('input')
 
344
        var prompt = document.getElementById("console_prompt");
 
345
        prompt.replaceChild(document.createTextNode("+++ "), prompt.firstChild);
 
346
    }
 
347
 
 
348
    if (inputbox != null)
 
349
    {
 
350
        /* Re-enable the text box */
 
351
        clearTimeout(graytimer);
 
352
        inputbox.removeAttribute("disabled");
 
353
        inputbox.removeAttribute("class");
 
354
        interrupted = false;
 
355
    }
 
356
 
 
357
    /* Open up the console so we can see the output */
 
358
    console_maximize();
 
359
    /* Auto-scrolling */
 
360
    divScroll.activeScroll();
 
361
 
 
362
    // Focus the input box by default
 
363
    document.getElementById("console_output").focus()
 
364
    document.getElementById("console_inputText").focus()
 
365
}
 
366
 
 
367
function catch_input(key)
 
368
{
 
369
    var inp = document.getElementById('console_inputText');
 
370
    switch (key)
 
371
    {
 
372
    case 9:                 /* Tab key */
 
373
        var selstart = inp.selectionStart;
 
374
        var selend = inp.selectionEnd;
 
375
        if (selstart == selend)
 
376
        {
 
377
            /* No selection, just a carat. Insert a tab here. */
 
378
            inp.value = inp.value.substr(0, selstart)
 
379
                + TAB_STRING + inp.value.substr(selstart);
 
380
        }
 
381
        else
 
382
        {
 
383
            /* Text is selected. Just indent the whole line
 
384
             * by inserting a tab at the start */
 
385
            inp.value = TAB_STRING + inp.value;
 
386
        }
 
387
        /* Update the selection so the same characters as before are selected
 
388
         */
 
389
        inp.selectionStart = selstart + TAB_STRING.length;
 
390
        inp.selectionEnd = inp.selectionStart + (selend - selstart);
 
391
        /* Cancel the event, so the TAB key doesn't move focus away from this
 
392
         * box */
 
393
        return false;
 
394
        /* Note: If it happens that some browsers don't support event
 
395
         * cancelling properly, this hack might work instead:
 
396
        setTimeout(
 
397
            "document.getElementById('console_inputText').focus()",
 
398
            0);
 
399
         */
 
400
        break;
 
401
    case 13:                /* Enter key */
 
402
        var callback = function()
 
403
        {
 
404
            /* Send the line of text to the server */
 
405
            console_enter_line(inp, "chat");
 
406
            hist.submit(inp.value);
 
407
            inp.value = hist.curr();
 
408
        }
 
409
        /* Start the server if it hasn't already been started */
 
410
        start_server(callback);
 
411
        break;
 
412
    case 38:                /* Up arrow */
 
413
        hist.up(inp.value);
 
414
        inp.value = hist.curr();
 
415
        break;
 
416
    case 40:                /* Down arrow */
 
417
        hist.down(inp.value);
 
418
        inp.value = hist.curr();
 
419
        break;
 
420
    }
 
421
}
 
422
 
 
423
/**** Following Code modified from ******************************************/
 
424
/**** http://radio.javaranch.com/pascarello/2006/08/17/1155837038219.html ***/
 
425
/****************************************************************************/
 
426
var chatscroll = new Object();
 
427
 
 
428
chatscroll.Pane = function(scrollContainerId)
 
429
{
 
430
    this.scrollContainerId = scrollContainerId;
 
431
}
 
432
 
 
433
chatscroll.Pane.prototype.activeScroll = function()
 
434
{
 
435
    var scrollDiv = document.getElementById(this.scrollContainerId);
 
436
    var currentHeight = 0;
 
437
        
 
438
    if (scrollDiv.scrollHeight > 0)
 
439
        currentHeight = scrollDiv.scrollHeight;
 
440
    else 
 
441
        if (objDiv.offsetHeight > 0)
 
442
            currentHeight = scrollDiv.offsetHeight;
 
443
 
 
444
    scrollDiv.scrollTop = currentHeight;
 
445
 
 
446
    scrollDiv = null;
 
447
}
 
448
 
 
449
var divScroll = new chatscroll.Pane('console_output');