summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--css/codeq/console.css2
-rw-r--r--index.html1
-rw-r--r--js/codeq/console.js351
-rw-r--r--js/codeq/hint.js193
-rw-r--r--js/codeq/startup.js1
-rw-r--r--js/prolog.js204
-rw-r--r--js/python.js203
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;
}
diff --git a/index.html b/index.html
index 9a5559b..5ca650a 100644
--- a/index.html
+++ b/index.html
@@ -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">&nbsp;</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;
+ }
+ };
};
})();
generated by cgit v1.2.1 (git 2.18.0) at 2024-06-30 23:34:52 +0000