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 /js/prolog.js | |
parent | 7009ae2c2dca4b70e903135f088a15acb95f5085 (diff) | |
parent | 31cc69df82abce2250505c1e088d3f787a521a13 (diff) |
XMerge branch 'master' of ssh://212.235.189.51:22122/codeq-web
Diffstat (limited to 'js/prolog.js')
-rw-r--r-- | js/prolog.js | 204 |
1 files changed, 20 insertions, 184 deletions
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; + } + }; }; })(); |