diff options
author | Robert Zorko <robertz@gurucue.com> | 2015-09-18 09:43:03 +0200 |
---|---|---|
committer | Robert Zorko <robertz@gurucue.com> | 2015-09-18 09:43:03 +0200 |
commit | 70298cba94e4de9b186758d72e6c293e92f0418f (patch) | |
tree | 10adb79ea116d9d4c8a2b6beaaca146b739cf8b1 | |
parent | 7009ae2c2dca4b70e903135f088a15acb95f5085 (diff) | |
parent | 31cc69df82abce2250505c1e088d3f787a521a13 (diff) |
XMerge branch 'master' of ssh://212.235.189.51:22122/codeq-web
-rw-r--r-- | css/codeq/console.css | 2 | ||||
-rw-r--r-- | index.html | 1 | ||||
-rw-r--r-- | js/codeq/console.js | 351 | ||||
-rw-r--r-- | js/codeq/hint.js | 193 | ||||
-rw-r--r-- | js/codeq/startup.js | 1 | ||||
-rw-r--r-- | js/prolog.js | 204 | ||||
-rw-r--r-- | js/python.js | 203 |
7 files changed, 503 insertions, 452 deletions
diff --git a/css/codeq/console.css b/css/codeq/console.css index 2f5e9cf..c8dd9fd 100644 --- a/css/codeq/console.css +++ b/css/codeq/console.css @@ -8,7 +8,7 @@ background-color: transparent; border: none; color: inherit; - line-height: inherit; + line-height: normal; margin: 0; padding: 0; } @@ -132,6 +132,7 @@ <script src="js/codeq/stateMachine.js"></script> <script src="js/codeq/comms.js"></script> <script src="js/codeq/console.js"></script> + <script src="js/codeq/hint.js"></script> <script src="js/def_parser.js"></script> <!-- <script src="js/codeq/prologPythonLib.js"></script> --> <script src="js/codeq/prolog.js"></script> diff --git a/js/codeq/console.js b/js/codeq/console.js index 99c1550..57d5a07 100644 --- a/js/codeq/console.js +++ b/js/codeq/console.js @@ -160,7 +160,7 @@ }; codeq.makeConsole = function (jqElt, options) { - var lines = [], // console content + var lines = [],// console content, line descriptors of the form {'content': 'string', 'classNames': [], 'jqLine': jQuery object, 'row': number} maxLines = (options && options.maxLines) || 10000, // how many lines to display at most currentRow = 0, // cursor position currentCol = 0, @@ -169,14 +169,72 @@ inputDisabled = false, // whether to ignore input lineBuffered = true, // whether we are line-buffered or not buffered + renderSpan = function (lineDescriptor, startCol, length) { + var jqLine = lineDescriptor.jqLine, + content = lineDescriptor.content, + classes = lineDescriptor.classNames, + endCol = startCol + length, + N = classes ? classes.length : 0, + i = 0, + spans = [], // what to render, items are of the form {'content': string, 'cssClass': string} + entry, classSpan, jq, span, s, prefixDelta, suffixDelta, e; + // seek out the first css class + while (i < N) { + entry = classes[i]; + if (((entry.start + entry.length) > startCol) && (entry.start < endCol)) break; + i++; + } + if (i < N) { + // render the first span + e = entry.start + entry.length; // end column of this css class + prefixDelta = entry.start < startCol ? startCol - entry.start : 0; + suffixDelta = e > endCol ? e - endCol : 0; + classSpan = entry.length - prefixDelta - suffixDelta; + span = {'content': content.substr(startCol, classSpan), 'cssClass': entry.name}; + spans.push(span); + startCol += classSpan; + i++; + // render the rest + while ((startCol < endCol) && (i < N)) { + entry = classes[i]; + e = entry.start + entry.length; // end column of this css class + prefixDelta = entry.start < startCol ? startCol - entry.start : 0; + suffixDelta = e > endCol ? e - endCol : 0; + classSpan = entry.length - prefixDelta - suffixDelta; + s = content.substr(startCol, classSpan); + if (entry.name === span.cssClass) { + span.content += s; // join content where the class is the same + } + else { + span = {'content': s, 'cssClass': entry.name}; + spans.push(span); + } + startCol += classSpan; + i++; + } + } + // render any leftover + if (startCol < endCol) { + entry = makeClassDescriptor('', startCol, endCol - startCol); + spans.push({'content': content.substring(startCol, endCol), 'cssClass': ''}); + } + // render spans + for (i = 0; i < spans.length; i++) { + span = spans[i]; + jq = $('<span class="cq-con-text ' + span.cssClass + '"></span>'); + jqLine.append(jq); + jq.text(span.content); + } + return entry; // return the last entry used + }, + renderLine = function (lineDescriptor) { var jqLine = lineDescriptor.jqLine, - className = 'cq-con-text ' + lineDescriptor.className, - content = lineDescriptor.content || '', - jq1, jq2, jqCursor; + content = lineDescriptor.content, + jqCursor, classDescriptor; if (!jqLine) { - jqLine = $('<pre class="cq-con-line ' + lineDescriptor.className + '"></pre>'); + jqLine = $('<pre class="cq-con-line"></pre>'); if (lineDescriptor.row == 0) { jqContent.prepend(jqLine); } @@ -196,36 +254,30 @@ if (currentRow == lineDescriptor.row) { // mark the cursor in the current line if (currentCol >= content.length) { - jq1 = $('<span class="' + className + '"></span>'); + // cursor after the last character + renderSpan(lineDescriptor, 0, content.length); jqCursor = $('<span class="cq-con-cursor"> </span>'); - jqLine.append(jq1); jqLine.append(jqCursor); - jq1.text(content); } else if (currentCol <= 0) { - jq2 = $('<span class="' + className + '"></span>'); - jqCursor = $('<span class="cq-con-cursor"></span>'); + // cursor at the first character + classDescriptor = lineDescriptor.classNames[0] || makeClassDescriptor('', 0, content.length); + jqCursor = $('<span class="cq-con-cursor ' + classDescriptor.name + '"></span>'); jqLine.append(jqCursor); - jqLine.append(jq2); jqCursor.text(content.charAt(0)); - jq2.text(content.substr(1)); + renderSpan(lineDescriptor, 1, content.length - 1); } else { - jq1 = $('<span class="' + className + '"></span>'); - jq2 = $('<span class="' + className + '"></span>'); - jqCursor = $('<span class="cq-con-cursor"></span>'); - jqLine.append(jq1); + // cursor somewhere in between + classDescriptor = renderSpan(lineDescriptor, 0, currentCol); + jqCursor = $('<span class="cq-con-cursor ' + classDescriptor.name + '"></span>'); jqLine.append(jqCursor); - jqLine.append(jq2); - jq1.text(content.substr(0, currentCol)); jqCursor.text(content.charAt(currentCol)); - jq2.text(content.substr(currentCol + 1)); + renderSpan(lineDescriptor, currentCol + 1, content.length - currentCol - 1); } } else { - jq1 = $('<span class="' + className + '"></span>'); - jqLine.append(jq1); - jq1.text(lineDescriptor.content); + renderSpan(lineDescriptor, 0, content.length); } }, @@ -259,6 +311,126 @@ return newLines; }, + makeClassDescriptor = function (name, start, length) { + return {'name': name, 'start': start, 'length': length}; + }, + + indexOfClassAtOrAfterColumn = function (classes, col) { + var N = classes.length, + i; + for (i = 0; i < N; i++) { + if (classes[i].start >= col) return i; + } + return N; + }, + + insertClass = function (classes, newClassName, startingCol, length) { + var newEntry = makeClassDescriptor(newClassName, startingCol, length), + endCol = startingCol + length, + i, N, prevClass, pos, auxEntry, delta; + // seek out the position where to insert the new class + i = indexOfClassAtOrAfterColumn(classes, startingCol); + prevClass = i > 0 ? classes[i-1] : null; + // insert the new class + classes.splice(i, 0, newEntry); + // if needed, adjust the length of the previous class + if (prevClass) { + pos = prevClass.start + prevClass.length; + if (pos > startingCol) { + // split the previous class in two, the new class gets inserted in between + delta = pos - startingCol; + auxEntry = makeClassDescriptor(prevClass.name, endCol, delta); + classes.splice(i+1, 0, auxEntry); + prevClass.length = prevClass.length - delta; + } + } + // readjust positions of the classes after the new one + N = classes.length; + for (i++; i < N; i++) { + auxEntry = classes[i]; + auxEntry.start = endCol; + endCol += auxEntry.length; + } + }, + + removeClasses = function (classes, startCol, length) { + var i, entry, endCol, e, prefixDelta, suffixDelta, N; + if (!length) return; + endCol = startCol + length; + for (i = classes.length - 1; i >= 0; i--) { + entry = classes[i]; + e = entry.start + entry.length; + if ((e > startCol) && (entry.start < endCol)) { + prefixDelta = entry.start < startCol ? startCol - entry.start : 0; + suffixDelta = e > endCol ? e - endCol : 0; + if ((prefixDelta == 0) && (suffixDelta == 0)) classes.splice(i, 1); + else entry.length = prefixDelta + suffixDelta; + } + } + // readjust positions + N = classes.length; + endCol = 0; + for (i = 0; i < N; i++) { + entry = classes[i]; + entry.start = endCol; + endCol += entry.length; + } + }, + + removeClassesBefore = function (classes, col) { + var i = indexOfClassAtOrAfterColumn(classes, col); + if (i == 0) return; // nothing to remove + classes.splice(0, i); + }, + + replaceClassesBeforeColumn = function (classes, col, newClassName, newLength) { + var i = indexOfClassAtOrAfterColumn(classes, col), + newEntry = makeClassDescriptor(newClassName, 0, newLength); + classes.splice(0, i, newEntry); + }, + + classesBetween = function (classes, startCol, endCol) { + var N = classes.length, + result = [], + i, e, entry, prefixDelta, suffixDelta; + for (i = 0; i < N; i++) { + entry = classes[i]; + e = entry.start + entry.length; // end column of this css class + if ((e > startCol) && (entry.start < endCol)) { + prefixDelta = entry.start < startCol ? startCol - entry.start : 0; + suffixDelta = e > endCol ? e - endCol : 0; + result.push(makeClassDescriptor(entry.name, entry.start + prefixDelta, entry.length - prefixDelta - suffixDelta)); + } + } + return result; + }, + + mergeClasses = function () { + var result = [], + i, arg, j, entry, endCol; + for (i = 0; i < arguments.length; i++) { + arg = arguments[i]; + if (arg instanceof Array) { + for (j = 0; j < arg.length; j++) result.push(arg[j]); + } + else result.push(arg); + } + // adjust positions of css classes + endCol = 0; + for (i = 0; i < result.length; i++) { + entry = result[i]; + entry.start = endCol; + endCol += entry.length; + } + return result; + }, + + scrollCursorIntoView = function () { + var dh = jqContent.height() - jqElt.height(); + if (dh > 0) + jqElt.scrollTop(dh); + }, + // the handler object that is returned handler = { 'setLineBuffered': function () { lineBuffered = true; }, @@ -309,14 +481,15 @@ 'insertRow': function (row, content, className, deferReflow) { // inserts a new row at the position specified - var lineDescriptor, i, jqLine; + var lineDescriptor, i; + if (!className) className = 'output'; for (i = lines.length; i < row; i++) { // insert any empty rows - lineDescriptor = {content: '', className: className, row: i}; + lineDescriptor = {content: '', classNames: [], row: i}; lines.push(lineDescriptor); if (!deferReflow) renderLine(lineDescriptor); } - lineDescriptor = {content: content, className: className, row: row}; + lineDescriptor = {content: content, classNames: content.length > 0 ? [makeClassDescriptor(className, 0, content.length)] : [], row: row}; if (row >= lines.length) lines.push(lineDescriptor); else lines.splice(row, 0, lineDescriptor); if (!deferReflow) this.reflow(row); @@ -324,7 +497,7 @@ }, 'splice': function (startRow, startCol, endRow, endCol, newText, className) { - var i, j, n, startLine, endLine, newLines, newTextLines, part1, part2; + var i, j, n, startLine, endLine, newLines, part1, part2, s, auxLine; if (!className) className = 'output'; // pre-process newText, convert it to newLines: an array of strings without newlines @@ -370,19 +543,25 @@ if (newLines.length > 1) { // the first and the last new lines are separate existing lines, modify them startLine.content = part1 + newLines[0]; + startLine.classNames = mergeClasses(classesBetween(startLine.classNames, 0, part1.length), makeClassDescriptor(className, part1.length, newLines[0].length)); if (startRow == endRow) { // we need to create one additional line to hold the compositum of the last line and part2 - this.insertRow(j, newLines[newLines.length - 1] + part2, className, true); + auxLine = this.insertRow(j, newLines[newLines.length - 1], className, true); + insertClass(auxLine.classNames, auxLine.content.length, part2.length); + auxLine.content = auxLine.content + part2; j++; } else { - endLine.content = newLines[newLines.length - 1] + part2; + s = newLines[newLines.length - 1]; + endLine.content = s + part2; + replaceClassesBeforeColumn(endLine.classNames, endCol, className, s.length); n--; // retain the last line } } else { // the first and the last new lines are the same existing line startLine.content = part1 + newLines[0] + part2; + startLine.classNames = mergeClasses(classesBetween(startLine.classNames, 0, part1.length), makeClassDescriptor(className, part1.length, newLines[0].length), classesBetween(endLine.classNames, endCol, endCol + part2.length)); } // remove the rest of the old lines while (n > 0) { @@ -422,7 +601,9 @@ startRow = lines.length - 1, i, lineDescriptor; if (newLines.length == 0) return; // nothing to do + if (typeof className !== 'string') className = 'output'; lineDescriptor = lines[startRow]; + insertClass(lineDescriptor.classNames, className, lineDescriptor.content.length, newLines[0].length); lineDescriptor.content = lineDescriptor.content + newLines[0]; for (i = 1; i < newLines.length; i++) { lineDescriptor = this.insertRow(startRow + i, newLines[i], className, true); @@ -441,20 +622,25 @@ part1 = currentContent.substring(0, currentCol), part2 = currentContent.substring(currentCol), newLines = formNewLines(text), - i, n; + i, n, auxLine; + if (typeof className !== 'string') className = 'output'; if (newLines.length == 0) return; // nothing to do else if (newLines.length == 1) { + insertClass(currentLine.classNames, className, part1.length, newLines[0].length); currentLine.content = part1 + newLines[0] + part2; if (!dontMoveCursor) currentCol += newLines[0].length; renderLine(currentLine); } else { + currentLine.classNames = mergeClasses(classesBetween(currentLine.classNames, 0, part1.length), makeClassDescriptor(className, part1.length, newLines[0].length)); currentLine.content = part1 + newLines[0]; n = newLines.length - 1; for (i = 1; i < n; i++) { this.insertRow(startRow + i, newLines[i], className, true); } - this.insertRow(startRow + n, newLines[n] + part2, className, true); + auxLine = this.insertRow(startRow + n, newLines[n], className, true); + insertClass(auxLine.classNames, auxLine.content.length, part2.length); + auxLine.content = auxLine.content + part2; if (!dontMoveCursor) { currentRow = startRow + n; currentCol = newLines[n].length; @@ -485,6 +671,7 @@ leftmost = typeof this.leftmostCol === 'number' && this.leftmostCol || 0; if ((currentCol > leftmost) && (currentCol <= content.length)) { currentCol--; + removeClasses(lineDescriptor.classNames, currentCol, 1); lineDescriptor.content = content.substring(0, currentCol) + content.substring(currentCol + 1); renderLine(lineDescriptor); } @@ -494,6 +681,7 @@ var lineDescriptor = lines[currentRow], content = lineDescriptor.content; if ((currentCol >= 0) && (currentCol < content.length)) { + removeClasses(lineDescriptor.classNames, currentCol, 1); lineDescriptor.content = content.substring(0, currentCol) + content.substring(currentCol + 1); renderLine(lineDescriptor); } @@ -554,10 +742,8 @@ handleInput = function (chars) { var isPastedFromClipboard = clipboardPasteInProgress || !aKeyIsDown, - newLines = chars.split('\n'), - N = newLines.length, - lastLineIndex = N - 1, - i, promise; + cookedChars = chars, // the default + cookedPromise, cookedLines, lastCookedLineIndex, i; if (inputDisabled || internallyDisabled) { // flatly ignore @@ -566,69 +752,70 @@ } internallyDisabled = true; - promise = Q(); + cookedPromise = Q(); - for (i = 0; i < N; i++) { - promise = promise - .then((function (newLine, lineIndex) {return function () { - var cookedChars = lineIndex < lastLineIndex ? newLine + '\n' : newLine, // default - thisRow = currentRow, - leftmost = typeof handler.leftmostCol === 'number' && handler.leftmostCol || 0, - dh; - - // first cook the input - if (typeof handler.onKeypress === 'function') { - // only invoke the handler if the newLine is not an empty string, otherwise cookedChars = '' - try { - cookedChars = cookedChars && handler.onKeypress(cookedChars, isPastedFromClipboard); - } - catch (e) { - codeq.log.error('Error during invocation of terminal onKeypress: ' + e, e); - } - } + // first cook the input + if (typeof handler.onKeypress === 'function') { + // only invoke the handler if the newLine is not an empty string, otherwise cookedChars = '' + try { + cookedChars = cookedChars && handler.onKeypress(cookedChars, isPastedFromClipboard); + } + catch (e) { + codeq.log.error('Error during invocation of terminal onKeypress: ' + e, e); + } + } - if (!cookedChars) { - // nothing to append - return; - } + if (typeof cookedChars !== 'string') cookedLines = ['']; + else cookedLines = cookedChars.split('\n'); + lastCookedLineIndex = cookedLines.length - 1; + + // now serve the cooking + for (i = 0; i <= lastCookedLineIndex; i++) { + cookedPromise = cookedPromise + .then(scrollCursorIntoView) // scroll to bottom on input + .then((function (cookedLine, cookedLineIndex) {return function () { + var thisRow = currentRow, + leftmost = typeof handler.leftmostCol === 'number' && handler.leftmostCol || 0; + + if (cookedLine) handler.insertAtCursor(cookedLine, 'input'); // append what we have to the display + if (cookedLineIndex < lastCookedLineIndex) { + // press on "enter" must be simulated -> jump to the start of the next line, which is first added + currentRow++; + currentCol = 0; + handler.insertRow(currentRow, '', 'input', true); + handler.reflow(currentRow - 1); // the previous line must be rendered without a cursor, and the new line must be rendered completely + } - // now serve the cooking - handler.insertAtCursor(cookedChars, 'input'); // append what we have to the display - // scroll to bottom on input - dh = jqContent.height() - jqElt.height(); - if (dh > 0) - jqElt.scrollTop(dh); - - if (typeof handler.onInput === 'function') { // now tell the owner what we've done - if (lineBuffered) { - if (thisRow < currentRow) { - // in line-buffered mode emit each line separately, except for the last (current) line + if (typeof handler.onInput === 'function') { // now tell the owner what we've done + if (lineBuffered) { + if (thisRow < currentRow) { + // in line-buffered mode emit each line separately, except for the last (current) line + try { + return handler.onInput(lines[thisRow].content.substring(leftmost)); + } + catch (e) { + codeq.log.error('Error while invoking terminal onInput: ' + e, e); + } + } + } + else if (cookedLine) { try { - return handler.onInput(lines[thisRow].content.substring(leftmost)); + return handler.onInput(cookedLine); } catch (e) { codeq.log.error('Error while invoking terminal onInput: ' + e, e); } } } - else if (cookedChars) { - try { - return handler.onInput(cookedChars); - } - catch (e) { - codeq.log.error('Error while invoking terminal onInput: ' + e, e); - } - } - } - - };})(newLines[i], i)) + };})(cookedLines[i], i)) .fail(function (e) { codeq.log.error('Error in handleInput loop: ' + e, e); }); } - promise.fin(function () { + cookedPromise.fin(function () { internallyDisabled = false; + scrollCursorIntoView(); }).done(); clipboardPasteInProgress = false; @@ -739,7 +926,7 @@ lines.push({content: options.greeting, className: 'greeting'}); currentRow++; } - lines.push({content: '', className: 'input'}); // initial input line + lines.push({content: '', classNames: []}); // initial input line render(); return handler; diff --git a/js/codeq/hint.js b/js/codeq/hint.js new file mode 100644 index 0000000..c22f39f --- /dev/null +++ b/js/codeq/hint.js @@ -0,0 +1,193 @@ +/** + * Creates a hint handler, displaying hints inside the provided jqHints <div>. + */ + +(function () { + // constants + var firstCharacterPos = {'line': 0, 'ch': 0}, + sel_no_scroll = {'scroll': false}; + + codeq.makeHinter = function (jqHints, jqEditor, editor, hintDefs) { + var hintCounter = 0, // for generating unique class-names + hintCleaners = [], + + clearHints = function () { + var i; + for (i = hintCleaners.length - 1; i >= 0; i--) { + hintCleaners[i](); + } + hintCleaners.length = 0; + hintCounter = 0; + }, + + addMark = function (start, end) { + var posStart = editor.posFromIndex(start), + posEnd = editor.posFromIndex(end), + doc = editor.getDoc(), + mark = doc.markText(posStart, posEnd, {'className': 'editor-mark _emark_' + hintCounter}), + result = {'start': posStart, 'end': posEnd, 'mark': mark, 'className': '_emark_' + hintCounter}; + hintCleaners.push(function () { mark.clear(); mark = null; doc = null; result.mark = null; }); + hintCounter++; + return result; + }, + + processTemplate = function (template, args) { + if (!args) + return template; + return template.replace(/\[%=(\w+)%\]/g, function(match, name) { + return args[name]; + }); + }, + + typeHandlers = { + 'static': function (type, template, serverHint) { + var jqContainer, jqButton, promise, i, lastIndex; + if (template instanceof Array) { // unwrap the template if there's only one + if (template.length == 0) template = ''; + else if (template.length == 1) template = template[0] + ''; + } + if (template instanceof Array) { + codeq.log.debug('Processing an array of static hints'); + jqContainer = $('<div class="hint-static-group"></div>'); + jqButton = $('<button type="button">More...</button>'); // TODO: translate "more" + jqHints.append(jqContainer); + lastIndex = template.length - 1; + promise = Q(); + for (i = 0; i <= lastIndex; i++) { + promise = promise.then((function (tmpl, index) { + return Q.Promise(function (resolve, reject) { + var message = processTemplate(tmpl, serverHint.args), + onClick; + jqContainer.append('<div class="hint-static">' + message + '</div>'); + if (index < lastIndex) { + onClick = function () { + jqButton.off('click', onClick); + jqButton.remove(); + resolve(); + }; + jqContainer.append(jqButton); + jqButton.on('click', onClick); + } + else { + resolve(); + } + }); + })(template[i], i)); + } + promise.done(); + } + else { + codeq.log.debug('Processing a single static hint'); + var message = processTemplate(template, serverHint.args); + jqHints.append('<div class="hint-static">' + message + '</div>'); + } + // no hint cleaner here, a static hint remains on the screen + }, + + 'popup': function (type, template, serverHint) { + codeq.log.debug('Processing popup hint'); + var message = processTemplate(template, serverHint.args), + mark = addMark(serverHint.start, serverHint.end), // add the mark + jqMark = jqEditor.find('.' + mark.className); + + jqMark.popover({'content': message, 'html': true, 'placement': 'auto bottom', 'trigger': 'hover focus click', 'container': 'body'}); + hintCleaners.push(function () { if (jqMark) { jqMark.popover('destroy'); jqMark = null; } }); + + mark.mark.on('', function () {}); + }, + + 'dropdown': function (type, template, serverHint) { + codeq.log.debug('Processing dropdown hint'); + var completion = null, // the completion object, created in showHint() + close = function () { + if (completion) { + completion.close(); + completion = null; + } + }; + + if (/*(editor.listSelections().length > 1) ||*/ editor.somethingSelected()) { + // showHint() doesn't work if a selection is activeparts + editor.setSelection(firstCharacterPos, firstCharacterPos, sel_no_scroll); // deselect anything + } + + editor.showHint({ + hint: function () { + var hints = { + list: serverHint.choices, + from: editor.posFromIndex(serverHint.start), + to: editor.posFromIndex(serverHint.end) + }; + completion = editor.state.completionActive; + return hints; + }, + completeOnSingleClick: true, + completeSingle: false + }); + + hintCleaners.push(close); + } + }; + + return { + /** + * Processes and display appropriately the server hints. + * TODO: sort hints so static and popup hints come first, and a (single) drop-down hint last + * + * @param {ServerHint[]} serverHints an array of hints from the server + */ + 'handle': function (serverHints) { + var n = serverHints.length, + /** number */ i, + /** ServerHint */ serverHint, + /** HintDefinition */ hintDef, + hintType, hintTemplate, t, fn, indices; + clearHints(); + mainLoop: + for (i = 0; i < n; i++) { + serverHint = serverHints[i]; + hintDef = hintDefs[serverHint.id]; + if (!hintDef) { + codeq.log.error('Undefined hint ' + serverHint.id); + continue; + } + if (serverHint.indices) { + indices = serverHint.indices; + for (i = 0; i < indices.length; i++) { + hintDef = hintDef[indices[i]]; + if (!hintDef) { + codeq.log.error('Undefined hint ' + serverHint.id + ' with indices ' + serverHint.indices); + continue mainLoop; + } + } + } + t = typeof hintDef; + if (t === 'object') { + hintType = hintDef.type; + hintTemplate = hintDef.message; + } + else if (t === 'string') { + hintType = 'static'; + hintTemplate = hintDef; + } + else { + codeq.log.error('Unsupported hint definition: ' + t); + continue; + } + + fn = typeHandlers[hintType]; + if (!fn) codeq.log.error('Unsupported hint type: ' + hintType); + else fn(hintType, hintTemplate, serverHint); + } + }, + + 'destroy': function () { + clearHints(); + jqHints.empty(); + jqHints = null; + jqEditor = null; + editor = null; + } + }; + }; +})();
\ No newline at end of file diff --git a/js/codeq/startup.js b/js/codeq/startup.js index 2f7df97..ccef9f9 100644 --- a/js/codeq/startup.js +++ b/js/codeq/startup.js @@ -77,6 +77,7 @@ $(document).ready(function () { }) .fail(function (reason) { $('#disabled').css('display', 'none'); + codeq.log.error('Login request failed: ' + reason, reason); alert('Login request failed: ' + reason); }) .done(); diff --git a/js/prolog.js b/js/prolog.js index 5406af4..1082392 100644 --- a/js/prolog.js +++ b/js/prolog.js @@ -9,6 +9,7 @@ //codeq.makePrologTerminalHandler = function (jqConsole, editor, problem_id, activityHandler) { var makePrologTerminalHandler = function (jqConsole, editor, problem_id, activityHandler) { var promptMode = true, // default: query composition; alternative: query result browsing + manualStop = false, // if the user stopped showing next answers (false) or if there are no more answers (true) terminal = codeq.makeConsole(jqConsole, { 'greeting': 'CodeQ Prolog terminal proxy' }), @@ -25,7 +26,7 @@ } if (promptMode) { terminal.setLineBuffered(); - terminal.append('.\n?- ', 'output'); + terminal.append(manualStop ? '?- ' : '.\n?- ', 'output'); } }, tcf = function terminalCommandFailed (error) { @@ -50,6 +51,7 @@ terminal.onInput = function (command) { if (promptMode) { promptMode = false; + manualStop = false; terminal.setNotBuffered(); return codeq.comms.sendQuery({ 'problem_id': problem_id, @@ -71,6 +73,7 @@ } else { // stop searching for answers + manualStop = true; return codeq.comms.sendQuery({ 'problem_id': problem_id, 'step': 'end', @@ -147,119 +150,7 @@ editor = CodeMirror(jqEditor[0], { cursorHeight: 0.85, lineNumbers: true, matchBrackets: true }), activityHandler = codeq.makeActivityHandler(editor, problem.id), terminal = makePrologTerminalHandler(jqConsole, editor, problem.id, activityHandler), - hintDefs = problem.hint, - hintCounter = 0, // for generating unique class-names - hintCleaners = [], - clearHints = function () { - var i; - for (i = hintCleaners.length - 1; i >= 0; i--) { - hintCleaners[i](); - } - hintCleaners.length = 0; - hintCounter = 0; - }, - addMark = function (start, end) { - var posStart = editor.posFromIndex(start), - posEnd = editor.posFromIndex(end), - doc = editor.getDoc(), - mark = doc.markText(posStart, posEnd, {className: 'editor-mark _emark_' + hintCounter}), - result = {start: posStart, end: posEnd, mark: mark, className: '_emark_' + hintCounter}; - hintCleaners.push(function () { mark.clear(); mark = null; doc = null; result.mark = null; }); - hintCounter++; - return result; - }, - processTemplate = function (template, args) { - if (!args) - return template; - return template.replace(/\[%=(\w+)%\]/g, function(match, name) { - return args[name]; - }); - }, - hintHandlers = { - 'static': function (type, template, serverHint) { - codeq.log.debug('Processing static hint'); - var message = processTemplate(template, serverHint.args); - jqHints.append('<div class="hint-static">' + message + '</div>'); - // no hint cleaner here, a static hint remains on the screen - }, - 'popup': function (type, template, serverHint) { - codeq.log.debug('Processing popup hint'); - var message = processTemplate(template, serverHint.args), - mark = addMark(serverHint.start, serverHint.end), // add the mark - jqMark = jqEditor.find('.' + mark.className); -/* jqPopup = null, - onBlur = function () { - codeq.log.debug('Removing popup'); - if (jqPopup) { - jqPopup.off('blur', onBlur); - jqPopup.remove(); - jqPopup = null; - } - }; - - window.jqMark = jqMark; // TODO: DEBUG - - jqMark.on('click', function () { - if (jqPopup) return; - codeq.log.debug('Showing popup'); - var pos = mark.mark.find(), // results in {from: {line: number, ch: number}, to: {line: number, ch: number}} - left = pos.from.ch < pos.to.ch ? pos.from.ch : pos.to.ch, - down = pos.from.line < pos.to.line ? pos.to.line : pos.from.line; - jqPopup = $('<div style="position: absolute;" class="editor-popup ' + mark.className + '"></div>').html(template); - editor.addWidget({line: down, ch: left}, jqPopup[0], true); - jqPopup = jqEditor.find('.editor-popup.' + mark.className); - setTimeout(function () {jqPopup.trigger('focus'); jqPopup.on('click', onBlur);}, 50); // event handlers can be registered only when the DOM elements is part of the document - window.jqPopup = jqPopup; // TODO: DEBUG - }); - - hintCleaners.push(function () { - if (jqPopup) { - jqPopup.off('blur', onBlur); - jqPopup.remove(); - jqPopup = null; - } - if (jqMark) { - jqMark = null; - } - mark = null; - });*/ - - jqMark.popover({content: message, html: true, placement: 'auto bottom', trigger: 'hover focus click', container: 'body'}); - hintCleaners.push(function () { if (jqMark) { jqMark.popover('destroy'); jqMark = null; } }); - - mark.mark.on('', function () {}); - }, - 'dropdown': function (type, template, serverHint) { - codeq.log.debug('Processing dropdown hint'); - var completion = null, // the completion object, created in showHint() - close = function () { - if (completion) { - completion.close(); - completion = null; - } - }; - - if ((editor.listSelections().length > 1) || editor.somethingSelected()) { - // showHint() doesn't work if a selection is activeparts - } - - editor.showHint({ - hint: function () { - var hints = { - list: serverHint.choices, - from: editor.posFromIndex(serverHint.start), - to: editor.posFromIndex(serverHint.end) - }; - completion = editor.state.completionActive; - return hints; - }, - completeOnSingleClick: true, - completeSingle: false - }); - - hintCleaners.push(close); - } - }; + hinter = codeq.makeHinter(jqHints, jqEditor, editor, problem.hint); editor.setValue(info.solution); $('#title').text(problem.slug); @@ -278,73 +169,6 @@ } }); - var handler = { - destroy: function () { - terminal.destroy(); - jqDescription.empty(); - jqEditor.empty(); // TODO: perhaps you do not want to "free" the editor, just empty it - jqConsole.empty(); // TODO: the same with the console - jqHints.empty(); // TODO: just make static references to these - jqDescription = null; - jqEditor = null; - jqConsole = null; - jqHints = null; - }, - - /** - * Processes and display appropriately the server hints. - * TODO: sort hints so static and popup hints come first, and a (single) drop-down hint last - * - * @param {ServerHint[]} serverHints an array of hints from the server - */ - processServerHints: function (serverHints) { - var n = serverHints.length, - /** number */ i, - /** ServerHint */ serverHint, - /** HintDefinition */ hintDef, - hintType, hintTemplate, t, fn; - clearHints(); - for (i = 0; i < n; i++) { - serverHint = serverHints[i]; - hintDef = hintDefs[serverHint.id]; - if (serverHint.indices) { - indices = serverHint.indices - for (i = 0; i < indices.length; i++) { - hintDef = hintDef[indices[i]]; - if (!hintDef) - break; - } - } - if (!hintDef) { - codeq.log.error('Undefined hint ' + serverHint.id + ' with indices ' + serverHint.indices); - continue; - } - t = typeof hintDef; - if (t === 'object') { - hintType = hintDef.type; - hintTemplate = hintDef.message; - } - else if (t === 'string') { - hintType = 'static'; - hintTemplate = hintDef; - } - else { - codeq.log.error('Unsupported hint definition: ' + t); - continue; - } - - fn = hintHandlers[hintType]; - if (!fn) codeq.log.error('Unsupported hint type: ' + hintType); - else fn(hintType, hintTemplate, serverHint); - } - } - }; - - var jqButtons = $('#block-toolbar button'); -// $(jqButtons.get(0)).on('click', function () { handler.processServerHints([{id:'x_must_be_female'}]); }); -// $(jqButtons.get(1)).on('click', function () { handler.processServerHints([{id:'popup_unknown', start: 20, end: 26}]); }); -// $(jqButtons.get(2)).on('click', function () { handler.processServerHints([{id:'drop_down', start: 20, end: 26, choices:['ena', 'dva', 'tri']}]); }); - $('#btn_code_hint').on('click', function () { terminal.append('hint.\n', 'input'); terminal.inputDisable(); @@ -357,7 +181,7 @@ .then( function hintSuccess(data) { if (data.code === 0) - handler.processServerHints(data.hints); + hinter.handle(data.hints); else terminal.append(data.message + '\n', 'error'); }, @@ -383,7 +207,7 @@ .then( function testSuccess(data) { if (data.code === 0) - handler.processServerHints(data.hints); + hinter.handle(data.hints); else terminal.append(data.message + '\n', 'error'); }, @@ -398,6 +222,18 @@ .done(); }); - return handler; + return { + destroy: function () { + hinter.destroy(); + terminal.destroy(); + jqDescription.empty(); + jqEditor.empty(); // TODO: perhaps you do not want to "free" the editor, just empty it + jqConsole.empty(); // TODO: the same with the console + jqDescription = null; + jqEditor = null; + jqConsole = null; + jqHints = null; + } + }; }; })(); diff --git a/js/python.js b/js/python.js index fd2b9b1..4a2ac92 100644 --- a/js/python.js +++ b/js/python.js @@ -65,7 +65,8 @@ 'queueTrace': function (trace) { trace['dt'] = deltaActivityMillis(); queue.push(trace); - if (ts === null) setTimeout(timer, 10000); // flush every 10 seconds + if (ts === null) ts = setTimeout(timer, 10000); // flush every 10 seconds + return this; }, 'flush': flush, 'addAndPurge': function (trace) { @@ -99,119 +100,7 @@ editor = CodeMirror(jqEditor[0], { cursorHeight: 0.85, lineNumbers: true, matchBrackets: true, mode: 'python' }), activityHandler = codeq.makeActivityHandler(editor, problem.id), terminal = makePythonTerminalHandler(jqConsole, editor, problem.id, activityHandler), - hintDefs = problem.hint, - hintCounter = 0, // for generating unique class-names - hintCleaners = [], - clearHints = function () { - var i; - for (i = hintCleaners.length - 1; i >= 0; i--) { - hintCleaners[i](); - } - hintCleaners.length = 0; - hintCounter = 0; - }, - addMark = function (start, end) { - var posStart = editor.posFromIndex(start), - posEnd = editor.posFromIndex(end), - doc = editor.getDoc(), - mark = doc.markText(posStart, posEnd, {className: 'editor-mark _emark_' + hintCounter}), - result = {start: posStart, end: posEnd, mark: mark, className: '_emark_' + hintCounter}; - hintCleaners.push(function () { mark.clear(); mark = null; doc = null; result.mark = null; }); - hintCounter++; - return result; - }, - processTemplate = function (template, args) { - if (!args) - return template; - return template.replace(/\[%=(\w+)%\]/g, function(match, name) { - return args[name]; - }); - }, - hintHandlers = { - 'static': function (type, template, serverHint) { - codeq.log.debug('Processing static hint'); - var message = processTemplate(template, serverHint.args); - jqHints.append('<div class="hint-static">' + message + '</div>'); - // no hint cleaner here, a static hint remains on the screen - }, - 'popup': function (type, template, serverHint) { - codeq.log.debug('Processing popup hint'); - var message = processTemplate(template, serverHint.args), - mark = addMark(serverHint.start, serverHint.end), // add the mark - jqMark = jqEditor.find('.' + mark.className); -/* jqPopup = null, - onBlur = function () { - codeq.log.debug('Removing popup'); - if (jqPopup) { - jqPopup.off('blur', onBlur); - jqPopup.remove(); - jqPopup = null; - } - }; - - window.jqMark = jqMark; // TODO: DEBUG - - jqMark.on('click', function () { - if (jqPopup) return; - codeq.log.debug('Showing popup'); - var pos = mark.mark.find(), // results in {from: {line: number, ch: number}, to: {line: number, ch: number}} - left = pos.from.ch < pos.to.ch ? pos.from.ch : pos.to.ch, - down = pos.from.line < pos.to.line ? pos.to.line : pos.from.line; - jqPopup = $('<div style="position: absolute;" class="editor-popup ' + mark.className + '"></div>').html(template); - editor.addWidget({line: down, ch: left}, jqPopup[0], true); - jqPopup = jqEditor.find('.editor-popup.' + mark.className); - setTimeout(function () {jqPopup.trigger('focus'); jqPopup.on('click', onBlur);}, 50); // event handlers can be registered only when the DOM elements is part of the document - window.jqPopup = jqPopup; // TODO: DEBUG - }); - - hintCleaners.push(function () { - if (jqPopup) { - jqPopup.off('blur', onBlur); - jqPopup.remove(); - jqPopup = null; - } - if (jqMark) { - jqMark = null; - } - mark = null; - });*/ - - jqMark.popover({content: message, html: true, placement: 'auto bottom', trigger: 'hover focus click', container: 'body'}); - hintCleaners.push(function () { if (jqMark) { jqMark.popover('destroy'); jqMark = null; } }); - - mark.mark.on('', function () {}); - }, - 'dropdown': function (type, template, serverHint) { - codeq.log.debug('Processing dropdown hint'); - var completion = null, // the completion object, created in showHint() - close = function () { - if (completion) { - completion.close(); - completion = null; - } - }; - - if ((editor.listSelections().length > 1) || editor.somethingSelected()) { - // showHint() doesn't work if a selection is activeparts - } - - editor.showHint({ - hint: function () { - var hints = { - list: serverHint.choices, - from: editor.posFromIndex(serverHint.start), - to: editor.posFromIndex(serverHint.end) - }; - completion = editor.state.completionActive; - return hints; - }, - completeOnSingleClick: true, - completeSingle: false - }); - - hintCleaners.push(close); - } - }; + hinter = codeq.makeHinter(jqHints, jqEditor, editor, problem.hint); editor.setValue(info.solution); $('#title').text(problem.slug); @@ -230,75 +119,7 @@ } }); - var handler = { - destroy: function () { - terminal.destroy(); - jqDescription.empty(); - jqEditor.empty(); // TODO: perhaps you do not want to "free" the editor, just empty it - jqConsole.empty(); // TODO: the same with the console - jqHints.empty(); // TODO: just make static references to these - jqDescription = null; - jqEditor = null; - jqConsole = null; - jqHints = null; - }, - - /** - * Processes and display appropriately the server hints. - * TODO: sort hints so static and popup hints come first, and a (single) drop-down hint last - * - * @param {ServerHint[]} serverHints an array of hints from the server - */ - processServerHints: function (serverHints) { - var n = serverHints.length, - /** number */ i, - /** ServerHint */ serverHint, - /** HintDefinition */ hintDef, - hintType, hintTemplate, t, fn; - clearHints(); - for (i = 0; i < n; i++) { - serverHint = serverHints[i]; - hintDef = hintDefs[serverHint.id]; - if (serverHint.indices) { - indices = serverHint.indices - for (i = 0; i < indices.length; i++) { - hintDef = hintDef[indices[i]]; - if (!hintDef) - break; - } - } - if (!hintDef) { - codeq.log.error('Undefined hint ' + serverHint.id + ' with indices ' + serverHint.indices); - continue; - } - t = typeof hintDef; - if (t === 'object') { - hintType = hintDef.type; - hintTemplate = hintDef.message; - } - else if (t === 'string') { - hintType = 'static'; - hintTemplate = hintDef; - } - else { - codeq.log.error('Unsupported hint definition: ' + t); - continue; - } - - fn = hintHandlers[hintType]; - if (!fn) codeq.log.error('Unsupported hint type: ' + hintType); - else fn(hintType, hintTemplate, serverHint); - } - } - }; - - var jqButtons = $('#block-toolbar button'); -// $(jqButtons.get(0)).on('click', function () { handler.processServerHints([{id:'x_must_be_female'}]); }); -// $(jqButtons.get(1)).on('click', function () { handler.processServerHints([{id:'popup_unknown', start: 20, end: 26}]); }); -// $(jqButtons.get(2)).on('click', function () { handler.processServerHints([{id:'drop_down', start: 20, end: 26, choices:['ena', 'dva', 'tri']}]); }); - $('#btn_code_hint').on('click', function () { -// handler.processServerHints([{id:'drop_down', start: 20, end: 26, choices:['ena', 'dva', 'tri']}]); var doc = editor.getDoc(); codeq.comms.sendHint({ 'language': 'python', @@ -307,7 +128,7 @@ }).then( function hintSuccess(data) { if (data.code === 0) - handler.processServerHints(data.hints); + hinter.handle(data.hints); else terminal.append('error: ' + data.message); }, @@ -325,7 +146,7 @@ }).then( function testSuccess(data) { if (data.code === 0) - handler.processServerHints(data.hints); + hinter.handle(data.hints); else terminal.append('error: ' + data.message); }, @@ -340,6 +161,18 @@ 'text': '' }); - return handler; + return { + destroy: function () { + hinter.destroy(); + terminal.destroy(); + jqDescription.empty(); + jqEditor.empty(); // TODO: perhaps you do not want to "free" the editor, just empty it + jqConsole.empty(); // TODO: the same with the console + jqDescription = null; + jqEditor = null; + jqConsole = null; + jqHints = null; + } + }; }; })(); |