← 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: dcoles
  • Date: 2008-03-10 06:11:51 UTC
  • Revision ID: svn-v3-trunk0:2b9c9e99-6f39-0410-b283-7f802c844ae2:trunk:682
Natural Language Tool Kit (nltk) for student code

setup.py: copy '/usr/share/nltk' into jail
d/s/install_proc.txt: How to download and install NLTK
d/dependencies.txt: Added NLTK as a student code dependancy

Show diffs side-by-side

added added

removed removed

Lines of Context:
www/media/console/console.js
63
63
            if (callback != null)
64
64
                callback();
65
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
 
    }
 
66
    ajax_call(callback1, "consoleservice", "start", {}, "POST");
91
67
}
92
68
 
93
69
/** Initialises the console. All apps which import console are required to
303
279
    var output = document.getElementById("console_output");
304
280
    if (res.hasOwnProperty('okay'))
305
281
    {
 
282
        // Success!
 
283
        if (res.okay)
 
284
        {
 
285
            output.appendChild(document.createTextNode(res.okay + "\n"));
 
286
            output.appendChild(span);
 
287
        }
306
288
        // set the prompt to >>>
307
289
        var prompt = document.getElementById("console_prompt");
308
290
        prompt.replaceChild(document.createTextNode(">>> "), prompt.firstChild);
319
301
        var prompt = document.getElementById("console_prompt");
320
302
        prompt.replaceChild(document.createTextNode(">>> "), prompt.firstChild);
321
303
    }
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
 
 
339
 
    }
340
304
    else if (res.hasOwnProperty('more'))
341
305
    {
342
306
        // Need more input, so set the prompt to ...