~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-01-29 23:38:20 UTC
  • Revision ID: svn-v3-trunk0:2b9c9e99-6f39-0410-b283-7f802c844ae2:trunk:328
console: Renamed HTML element IDs to prefix "console_".
    Reason: To facilitate plugging the console into other apps. Need to avoid
    naming conflicts.
    console.css and console.js: Updated references to these IDs.
tutorial: Minor changes to get XHTML to validate.
tutorialservice: Minor comment typo.

Show diffs side-by-side

added added

removed removed

Lines of Context:
103
103
 
104
104
function enter_line()
105
105
{
106
 
    var inp = document.getElementById('inputText');
 
106
    var inp = document.getElementById('console_inputText');
107
107
    var digest = hex_md5(inp.value + magic);
108
108
    var args = {"host": server_host, "port": server_port,
109
109
                    "digest":digest, "text":inp.value};
110
110
    var xmlhttp = ajax_call("consoleservice", "chat", args, "POST");
111
111
 
112
112
    var res = JSON.parse(xmlhttp.responseText);
113
 
    var output = document.getElementById("output");
 
113
    var output = document.getElementById("console_output");
114
114
    {
115
115
        var pre = document.createElement("pre");
116
116
        pre.setAttribute("class", "inputMsg");
134
134
            output.appendChild(pre);
135
135
        }
136
136
        // set the prompt to >>>
137
 
        var prompt = document.getElementById("prompt");
 
137
        var prompt = document.getElementById("console_prompt");
138
138
        prompt.replaceChild(document.createTextNode(">>> "), prompt.firstChild);
139
139
    }
140
140
    else if (res.hasOwnProperty('exc'))
149
149
    else if (res.hasOwnProperty('more'))
150
150
    {
151
151
        // Need more input, so set the prompt to ...
152
 
        var prompt = document.getElementById("prompt");
 
152
        var prompt = document.getElementById("console_prompt");
153
153
        prompt.replaceChild(document.createTextNode("... "), prompt.firstChild);
154
154
    }
155
155
    else {
156
156
        // assert res.hasOwnProperty('input')
157
 
        var prompt = document.getElementById("prompt");
 
157
        var prompt = document.getElementById("console_prompt");
158
158
        prompt.replaceChild(document.createTextNode("+++ "), prompt.firstChild);
159
159
    }
160
160
}
161
161
 
162
162
function catch_input(key)
163
163
{
164
 
    var inp = document.getElementById('inputText');
 
164
    var inp = document.getElementById('console_inputText');
165
165
    if (key == 13)
166
166
    {
167
167
        enter_line();