From 5f8015714f94a7d1785cf148c257d3be72d1e6c9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ale=C5=A1=20Smodi=C5=A1?= Date: Mon, 13 Jul 2015 17:56:49 +0200 Subject: Initial commit: bare page for Prolog tasks with editor and command prompt, lightweight task definition parser of pythonic assignment statements. --- js/lib/jquery.console.js | 773 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 773 insertions(+) create mode 100644 js/lib/jquery.console.js (limited to 'js/lib/jquery.console.js') diff --git a/js/lib/jquery.console.js b/js/lib/jquery.console.js new file mode 100644 index 0000000..4a75a99 --- /dev/null +++ b/js/lib/jquery.console.js @@ -0,0 +1,773 @@ +// JQuery Console 1.0 +// Sun Feb 21 20:28:47 GMT 2010 +// +// Copyright 2010 Chris Done, Simon David Pratt. All rights reserved. +// +// Redistribution and use in source and binary forms, with or without +// modification, are permitted provided that the following conditions +// are met: +// +// 1. Redistributions of source code must retain the above +// copyright notice, this list of conditions and the following +// disclaimer. +// +// 2. Redistributions in binary form must reproduce the above +// copyright notice, this list of conditions and the following +// disclaimer in the documentation and/or other materials +// provided with the distribution. +// +// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS +// FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE +// COPYRIGHT HOLDERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, +// INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, +// BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; +// LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +// CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT +// LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN +// ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE +// POSSIBILITY OF SUCH DAMAGE. + +// TESTED ON +// Internet Explorer 6 +// Opera 10.01 +// Chromium 4.0.237.0 (Ubuntu build 31094) +// Firefox 3.5.8, 3.6.2 (Mac) +// Safari 4.0.5 (6531.22.7) (Mac) +// Google Chrome 5.0.375.55 (Mac) + +(function($){ + var isWebkit = !!~navigator.userAgent.indexOf(' AppleWebKit/'); + + $.fn.console = function(config){ + //////////////////////////////////////////////////////////////////////// + // Constants + // Some are enums, data types, others just for optimisation + var keyCodes = { + // left + 37: moveBackward, + // right + 39: moveForward, + // up + 38: previousHistory, + // down + 40: nextHistory, + // backspace + 8: backDelete, + // delete + 46: forwardDelete, + // end + 35: moveToEnd, + // start + 36: moveToStart, + // return + 13: commandTrigger, + // tab + 18: doNothing, + // tab + 9: doComplete + }; + var ctrlCodes = { + // C-a + 65: moveToStart, + // C-e + 69: moveToEnd, + // C-d + 68: forwardDelete, + // C-n + 78: nextHistory, + // C-p + 80: previousHistory, + // C-b + 66: moveBackward, + // C-f + 70: moveForward, + // C-k + 75: deleteUntilEnd + }; + if(config.ctrlCodes) { + $.extend(ctrlCodes, config.ctrlCodes); + } + var altCodes = { + // M-f + 70: moveToNextWord, + // M-b + 66: moveToPreviousWord, + // M-d + 68: deleteNextWord + }; + var shiftCodes = { + // return + 13: newLine, + }; + var cursor = ' '; + + //////////////////////////////////////////////////////////////////////// + // Globals + var container = $(this); + var inner = $('
'); + // erjiang: changed this from a text input to a textarea so we + // can get pasted newlines + var typer = $(''); + // Prompt + var promptBox; + var prompt; + var continuedPromptLabel = config && config.continuedPromptLabel? + config.continuedPromptLabel : "> "; + var column = 0; + var promptText = ''; + var restoreText = ''; + var continuedText = ''; + var fadeOnReset = config.fadeOnReset !== undefined ? config.fadeOnReset : true; + // Prompt history stack + var history = []; + var ringn = 0; + // For reasons unknown to The Sword of Michael himself, Opera + // triggers and sends a key character when you hit various + // keys like PgUp, End, etc. So there is no way of knowing + // when a user has typed '#' or End. My solution is in the + // typer.keydown and typer.keypress functions; I use the + // variable below to ignore the keypress event if the keydown + // event succeeds. + var cancelKeyPress = 0; + // When this value is false, the prompt will not respond to input + var acceptInput = true; + // When this value is true, the command has been canceled + var cancelCommand = false; + + // External exports object + var extern = {}; + + //////////////////////////////////////////////////////////////////////// + // Main entry point + (function(){ + extern.promptLabel = config && config.promptLabel? config.promptLabel : "> "; + container.append(inner); + inner.append(typer); + typer.css({position:'absolute',top:0,left:'-9999px'}); + if (config.welcomeMessage) + message(config.welcomeMessage,'jquery-console-welcome'); + newPromptBox(); + if (config.autofocus) { + inner.addClass('jquery-console-focus'); + typer.focus(); + setTimeout(function(){ + inner.addClass('jquery-console-focus'); + typer.focus(); + },100); + } + extern.inner = inner; + extern.typer = typer; + extern.scrollToBottom = scrollToBottom; + extern.report = report; + })(); + + //////////////////////////////////////////////////////////////////////// + // Reset terminal + extern.reset = function(){ + var welcome = (typeof config.welcomeMessage != 'undefined'); + + var removeElements = function() { + inner.find('div').each(function(){ + if (!welcome) { + $(this).remove(); + } else { + welcome = false; + } + }); + }; + + if (fadeOnReset) { + inner.parent().fadeOut(function() { + removeElements(); + newPromptBox(); + inner.parent().fadeIn(focusConsole); + }); + } + else { + removeElements(); + newPromptBox(); + focusConsole(); + } + }; + + var focusConsole = function() { + inner.addClass('jquery-console-focus'); + typer.focus(); + }; + + extern.focus = function(){ + focusConsole(); + } + + //////////////////////////////////////////////////////////////////////// + // Reset terminal + extern.notice = function(msg,style){ + var n = $('
').append($('
').text(msg)) + .css({visibility:'hidden'}); + container.append(n); + var focused = true; + if (style=='fadeout') + setTimeout(function(){ + n.fadeOut(function(){ + n.remove(); + }); + },4000); + else if (style=='prompt') { + var a = $('
OK
'); + n.append(a); + focused = false; + a.click(function(){ n.fadeOut(function(){ n.remove();inner.css({opacity:1}) }); }); + } + var h = n.height(); + n.css({height:'0px',visibility:'visible'}) + .animate({height:h+'px'},function(){ + if (!focused) inner.css({opacity:0.5}); + }); + n.css('cursor','default'); + return n; + }; + + //////////////////////////////////////////////////////////////////////// + // Make a new prompt box + function newPromptBox() { + column = 0; + promptText = ''; + ringn = 0; // Reset the position of the history ring + enableInput(); + promptBox = $('
'); + var label = $(''); + var labelText = extern.continuedPrompt? continuedPromptLabel : extern.promptLabel; + promptBox.append(label.text(labelText).show()); + label.html(label.html().replace(' ',' ')); + prompt = $(''); + promptBox.append(prompt); + inner.append(promptBox); + updatePromptDisplay(); + }; + + //////////////////////////////////////////////////////////////////////// + // Handle setting focus + container.click(function(){ + // Don't mess with the focus if there is an active selection + if (window.getSelection().toString()) { + return false; + } + + inner.addClass('jquery-console-focus'); + inner.removeClass('jquery-console-nofocus'); + if (isWebkit) { + typer.focusWithoutScrolling(); + } else { + typer.css('position', 'fixed').focus(); + } + scrollToBottom(); + return false; + }); + + //////////////////////////////////////////////////////////////////////// + // Handle losing focus + typer.blur(function(){ + inner.removeClass('jquery-console-focus'); + inner.addClass('jquery-console-nofocus'); + }); + + //////////////////////////////////////////////////////////////////////// + // Bind to the paste event of the input box so we know when we + // get pasted data + typer.bind('paste', function(e) { + // wipe typer input clean just in case + typer.val(""); + // this timeout is required because the onpaste event is + // fired *before* the text is actually pasted + setTimeout(function() { + typer.consoleInsert(typer.val()); + typer.val(""); + }, 0); + }); + + //////////////////////////////////////////////////////////////////////// + // Handle key hit before translation + // For picking up control characters like up/left/down/right + + typer.keydown(function(e){ + cancelKeyPress = 0; + var keyCode = e.keyCode; + // C-c: cancel the execution + if(e.ctrlKey && keyCode == 67) { + cancelKeyPress = keyCode; + cancelExecution(); + return false; + } + if (acceptInput) { + if (e.shiftKey && keyCode in shiftCodes) { + cancelKeyPress = keyCode; + (shiftCodes[keyCode])(); + return false; + } else if (e.altKey && keyCode in altCodes) { + cancelKeyPress = keyCode; + (altCodes[keyCode])(); + return false; + } else if (e.ctrlKey && keyCode in ctrlCodes) { + cancelKeyPress = keyCode; + (ctrlCodes[keyCode])(); + return false; + } else if (keyCode in keyCodes) { + cancelKeyPress = keyCode; + (keyCodes[keyCode])(); + return false; + } + } + }); + + //////////////////////////////////////////////////////////////////////// + // Handle key press + typer.keypress(function(e){ + var keyCode = e.keyCode || e.which; + if (isIgnorableKey(e)) { + return false; + } + // C-v: don't insert on paste event + if ((e.ctrlKey || e.metaKey) && String.fromCharCode(keyCode).toLowerCase() == 'v') { + return true; + } + if (acceptInput && cancelKeyPress != keyCode && keyCode >= 32){ + if (cancelKeyPress) return false; + if ( + typeof config.charInsertTrigger == 'undefined' || ( + typeof config.charInsertTrigger == 'function' && + config.charInsertTrigger(keyCode,promptText) + ) + ){ + typer.consoleInsert(keyCode); + } + } + if (isWebkit) return false; + }); + + function isIgnorableKey(e) { + // for now just filter alt+tab that we receive on some platforms when + // user switches windows (goes away from the browser) + return ((e.keyCode == keyCodes.tab || e.keyCode == 192) && e.altKey); + }; + + //////////////////////////////////////////////////////////////////////// + // Rotate through the command history + function rotateHistory(n){ + if (history.length == 0) return; + ringn += n; + if (ringn < 0) ringn = history.length; + else if (ringn > history.length) ringn = 0; + var prevText = promptText; + if (ringn == 0) { + promptText = restoreText; + } else { + promptText = history[ringn - 1]; + } + if (config.historyPreserveColumn) { + if (promptText.length < column + 1) { + column = promptText.length; + } else if (column == 0) { + column = promptText.length; + } + } else { + column = promptText.length; + } + updatePromptDisplay(); + }; + + function previousHistory() { + rotateHistory(-1); + }; + + function nextHistory() { + rotateHistory(1); + }; + + // Add something to the history ring + function addToHistory(line){ + history.push(line); + restoreText = ''; + }; + + // Delete the character at the current position + function deleteCharAtPos(){ + if (column < promptText.length){ + promptText = + promptText.substring(0,column) + + promptText.substring(column+1); + restoreText = promptText; + return true; + } else return false; + }; + + function backDelete() { + if (moveColumn(-1)){ + deleteCharAtPos(); + updatePromptDisplay(); + } + }; + + function forwardDelete() { + if (deleteCharAtPos()){ + updatePromptDisplay(); + } + }; + + function deleteUntilEnd() { + while(deleteCharAtPos()) { + updatePromptDisplay(); + } + }; + + function deleteNextWord() { + // A word is defined within this context as a series of alphanumeric + // characters. + // Delete up to the next alphanumeric character + while( + column < promptText.length && + !isCharAlphanumeric(promptText[column]) + ) { + deleteCharAtPos(); + updatePromptDisplay(); + } + // Then, delete until the next non-alphanumeric character + while( + column < promptText.length && + isCharAlphanumeric(promptText[column]) + ) { + deleteCharAtPos(); + updatePromptDisplay(); + } + }; + + function newLine() { + var lines = promptText.split("\n"); + var last_line = lines.slice(-1)[0]; + var spaces = last_line.match(/^(\s*)/g)[0]; + var new_line = "\n" + spaces; + promptText += new_line; + moveColumn(new_line.length); + updatePromptDisplay(); + }; + + //////////////////////////////////////////////////////////////////////// + // Validate command and trigger it if valid, or show a validation error + function commandTrigger() { + var line = promptText; + if (typeof config.commandValidate == 'function') { + var ret = config.commandValidate(line); + if (ret == true || ret == false) { + if (ret) { + handleCommand(); + } + } else { + commandResult(ret,"jquery-console-message-error"); + } + } else { + handleCommand(); + } + }; + + // Scroll to the bottom of the view + function scrollToBottom() { + var version = jQuery.fn.jquery.split('.'); + var major = parseInt(version[0]); + var minor = parseInt(version[1]); + + // check if we're using jquery > 1.6 + if ((major == 1 && minor > 6) || major > 1) { + inner.prop({ scrollTop: inner.prop("scrollHeight") }); + } + else { + inner.attr({ scrollTop: inner.attr("scrollHeight") }); + } + }; + + function cancelExecution() { + if(typeof config.cancelHandle == 'function') { + config.cancelHandle(); + } + } + + //////////////////////////////////////////////////////////////////////// + // Handle a command + function handleCommand() { + if (typeof config.commandHandle == 'function') { + disableInput(); + addToHistory(promptText); + var text = promptText; + if (extern.continuedPrompt) { + if (continuedText) + continuedText += '\n' + promptText; + else continuedText = promptText; + } else continuedText = undefined; + if (continuedText) text = continuedText; + var ret = config.commandHandle(text,function(msgs){ + commandResult(msgs); + }); + if (extern.continuedPrompt && !continuedText) + continuedText = promptText; + if (typeof ret == 'boolean') { + if (ret) { + // Command succeeded without a result. + commandResult(); + } else { + commandResult( + 'Command failed.', + "jquery-console-message-error" + ); + } + } else if (typeof ret == "string") { + commandResult(ret,"jquery-console-message-success"); + } else if (typeof ret == 'object' && ret.length) { + commandResult(ret); + } else if (extern.continuedPrompt) { + commandResult(); + } + } + }; + + //////////////////////////////////////////////////////////////////////// + // Disable input + function disableInput() { + acceptInput = false; + }; + + // Enable input + function enableInput() { + acceptInput = true; + } + + //////////////////////////////////////////////////////////////////////// + // Reset the prompt in invalid command + function commandResult(msg,className) { + column = -1; + updatePromptDisplay(); + if (typeof msg == 'string') { + message(msg,className); + } else if ($.isArray(msg)) { + for (var x in msg) { + var ret = msg[x]; + message(ret.msg,ret.className); + } + } else { // Assume it's a DOM node or jQuery object. + inner.append(msg); + } + newPromptBox(); + }; + + //////////////////////////////////////////////////////////////////////// + // Report some message into the console + function report(msg,className) { + var text = promptText; + promptBox.remove(); + commandResult(msg,className); + extern.promptText(text); + }; + + //////////////////////////////////////////////////////////////////////// + // Display a message + function message(msg,className) { + var mesg = $('
'); + if (className) mesg.addClass(className); + mesg.filledText(msg).hide(); + inner.append(mesg); + mesg.show(); + }; + + //////////////////////////////////////////////////////////////////////// + // Handle normal character insertion + // data can either be a number, which will be interpreted as the + // numeric value of a single character, or a string + typer.consoleInsert = function(data){ + // TODO: remove redundant indirection + var text = (typeof data == 'number') ? String.fromCharCode(data) : data; + var before = promptText.substring(0,column); + var after = promptText.substring(column); + promptText = before + text + after; + moveColumn(text.length); + restoreText = promptText; + updatePromptDisplay(); + }; + + //////////////////////////////////////////////////////////////////////// + // Move to another column relative to this one + // Negative means go back, positive means go forward. + function moveColumn(n){ + if (column + n >= 0 && column + n <= promptText.length){ + column += n; + return true; + } else return false; + }; + + function moveForward() { + if(moveColumn(1)) { + updatePromptDisplay(); + return true; + } + return false; + }; + + function moveBackward() { + if(moveColumn(-1)) { + updatePromptDisplay(); + return true; + } + return false; + }; + + function moveToStart() { + if (moveColumn(-column)) + updatePromptDisplay(); + }; + + function moveToEnd() { + if (moveColumn(promptText.length-column)) + updatePromptDisplay(); + }; + + function moveToNextWord() { + while( + column < promptText.length && + !isCharAlphanumeric(promptText[column]) && + moveForward() + ) {} + while( + column < promptText.length && + isCharAlphanumeric(promptText[column]) && + moveForward() + ) {} + }; + + function moveToPreviousWord() { + // Move backward until we find the first alphanumeric + while( + column -1 >= 0 && + !isCharAlphanumeric(promptText[column-1]) && + moveBackward() + ) {} + // Move until we find the first non-alphanumeric + while( + column -1 >= 0 && + isCharAlphanumeric(promptText[column-1]) && + moveBackward() + ) {} + }; + + function isCharAlphanumeric(charToTest) { + if(typeof charToTest == 'string') { + var code = charToTest.charCodeAt(); + return (code >= 'A'.charCodeAt() && code <= 'Z'.charCodeAt()) || + (code >= 'a'.charCodeAt() && code <= 'z'.charCodeAt()) || + (code >= '0'.charCodeAt() && code <= '9'.charCodeAt()); + } + return false; + }; + + function doComplete() { + if(typeof config.completeHandle == 'function') { + var completions = config.completeHandle(promptText); + var len = completions.length; + if (len === 1) { + extern.promptText(promptText + completions[0]); + } else if (len > 1 && config.cols) { + var prompt = promptText; + // Compute the number of rows that will fit in the width + var max = 0; + for (var i = 0;i < len;i++) { + max = Math.max(max, completions[i].length); + } + max += 2; + var n = Math.floor(config.cols / max); + var buffer = ""; + var col = 0; + for (i = 0;i < len;i++) { + var completion = completions[i]; + buffer += completions[i]; + for (var j = completion.length;j < max;j++) { + buffer += " "; + } + if (++col >= n) { + buffer += "\n"; + col = 0; + } + } + commandResult(buffer,"jquery-console-message-value"); + extern.promptText(prompt); + } + } + }; + + function doNothing() {}; + + extern.promptText = function(text){ + if (typeof text === 'string') { + promptText = text; + column = promptText.length; + updatePromptDisplay(); + } + return promptText; + }; + + //////////////////////////////////////////////////////////////////////// + // Update the prompt display + function updatePromptDisplay(){ + var line = promptText; + var html = ''; + if (column > 0 && line == ''){ + // When we have an empty line just display a cursor. + html = cursor; + } else if (column == promptText.length){ + // We're at the end of the line, so we need to display + // the text *and* cursor. + html = htmlEncode(line) + cursor; + } else { + // Grab the current character, if there is one, and + // make it the current cursor. + var before = line.substring(0, column); + var current = line.substring(column,column+1); + if (current){ + current = + '' + + htmlEncode(current) + + ''; + } + var after = line.substring(column+1); + html = htmlEncode(before) + current + htmlEncode(after); + } + prompt.html(html); + scrollToBottom(); + }; + + // Simple HTML encoding + // Simply replace '<', '>' and '&' + // TODO: Use jQuery's .html() trick, or grab a proper, fast + // HTML encoder. + function htmlEncode(text){ + return ( + text.replace(/&/g,'&') + .replace(/') + ); + }; + + return extern; + }; + // Simple utility for printing messages + $.fn.filledText = function(txt){ + $(this).text(txt); + $(this).html($(this).html().replace(/\n/g,'
')); + return this; + }; + + // Alternative method for focus without scrolling + $.fn.focusWithoutScrolling = function(){ + var x = window.scrollX, y = window.scrollY; + $(this).focus(); + window.scrollTo(x, y); + }; +})(jQuery); -- cgit v1.2.1