ihaskell-parsec 0.2.0.0 → 0.2.1.0
raw patch · 3 files changed
+296/−1 lines, 3 files
Files
- ihaskell-parsec.cabal +2/−1
- widget.html +6/−0
- widget.js +288/−0
ihaskell-parsec.cabal view
@@ -7,7 +7,7 @@ -- PVP summary: +-+------- breaking API changes -- | | +----- non-breaking API additions -- | | | +--- code changes with no API change-version: 0.2.0.0+version: 0.2.1.0 -- A short (one-line) description of the package. synopsis: IHaskell display instances for Parsec@@ -38,6 +38,7 @@ build-type: Simple +extra-source-files: widget.html, widget.js -- Extra files to be distributed with the package, such as examples or a -- README. -- extra-source-files:
+ widget.html view
@@ -0,0 +1,6 @@+<!-- CodeMirror component -->+<link rel="stylesheet" href="/static/components/codemirror/addon/lint/lint.css">++<!-- Parsec widget DOM -->+<form><textarea id="parsec-editor">Insert parser text here...</textarea></form>+<pre id="parsec-output"></pre>
+ widget.js view
@@ -0,0 +1,288 @@+// Only load this script once.+var kernel = IPython.notebook.kernel;+var initialized = kernel !== undefined && kernel != null;+console.log("Initialized", initialized);+if (initialized && window.parsecWidgetRegistered === undefined) {++// Do not load this script again.+window.parsecWidgetRegistered = true;++// Codemirror lint.js+// Must be included here, otherwise linting cannot happen the first time the widget is loaded.+(function() {+ "use strict";+ var GUTTER_ID = "CodeMirror-lint-markers";+ var SEVERITIES = /^(?:error|warning)$/;++ function showTooltip(e, content) {+ var tt = document.createElement("div");+ tt.className = "CodeMirror-lint-tooltip";+ tt.appendChild(content.cloneNode(true));+ document.body.appendChild(tt);++ function position(e) {+ if (!tt.parentNode) return CodeMirror.off(document, "mousemove", position);+ tt.style.top = Math.max(0, e.clientY - tt.offsetHeight - 5) + "px";+ tt.style.left = (e.clientX + 5) + "px";+ }+ CodeMirror.on(document, "mousemove", position);+ position(e);+ if (tt.style.opacity != null) tt.style.opacity = 1;+ return tt;+ }+ function rm(elt) {+ if (elt.parentNode) elt.parentNode.removeChild(elt);+ }+ function hideTooltip(tt) {+ if (!tt.parentNode) return;+ if (tt.style.opacity == null) rm(tt);+ tt.style.opacity = 0;+ setTimeout(function() { rm(tt); }, 600);+ }++ function showTooltipFor(e, content, node) {+ var tooltip = showTooltip(e, content);+ function hide() {+ CodeMirror.off(node, "mouseout", hide);+ if (tooltip) { hideTooltip(tooltip); tooltip = null; }+ }+ var poll = setInterval(function() {+ if (tooltip) for (var n = node;; n = n.parentNode) {+ if (n == document.body) return;+ if (!n) { hide(); break; }+ }+ if (!tooltip) return clearInterval(poll);+ }, 400);+ CodeMirror.on(node, "mouseout", hide);+ }++ function LintState(cm, options, hasGutter) {+ this.marked = [];+ this.options = options;+ this.timeout = null;+ this.hasGutter = hasGutter;+ this.onMouseOver = function(e) { onMouseOver(cm, e); };+ }++ function parseOptions(cm, options) {+ if (options instanceof Function) return {getAnnotations: options};+ if (!options || options === true) options = {};+ if (!options.getAnnotations) options.getAnnotations = cm.getHelper(CodeMirror.Pos(0, 0), "lint");+ if (!options.getAnnotations) throw new Error("Required option 'getAnnotations' missing (lint addon)");+ return options;+ }++ function clearMarks(cm) {+ var state = cm.state.lint;+ if (state.hasGutter) cm.clearGutter(GUTTER_ID);+ for (var i = 0; i < state.marked.length; ++i)+ state.marked[i].clear();+ state.marked.length = 0;+ }++ function makeMarker(labels, severity, multiple, tooltips) {+ var marker = document.createElement("div"), inner = marker;+ marker.className = "CodeMirror-lint-marker-" + severity;+ if (multiple) {+ inner = marker.appendChild(document.createElement("div"));+ inner.className = "CodeMirror-lint-marker-multiple";+ }++ if (tooltips != false) CodeMirror.on(inner, "mouseover", function(e) {+ showTooltipFor(e, labels, inner);+ });++ return marker;+ }++ function getMaxSeverity(a, b) {+ if (a == "error") return a;+ else return b;+ }++ function groupByLine(annotations) {+ var lines = [];+ for (var i = 0; i < annotations.length; ++i) {+ var ann = annotations[i], line = ann.from.line;+ (lines[line] || (lines[line] = [])).push(ann);+ }+ return lines;+ }++ function annotationTooltip(ann) {+ var severity = ann.severity;+ if (!SEVERITIES.test(severity)) severity = "error";+ var tip = document.createElement("div");+ tip.className = "CodeMirror-lint-message-" + severity;+ tip.appendChild(document.createTextNode(ann.message));+ return tip;+ }++ function startLinting(cm) {+ var state = cm.state.lint, options = state.options;+ if (options.async)+ options.getAnnotations(cm, updateLinting, options);+ else+ updateLinting(cm, options.getAnnotations(cm.getValue(), options.options));+ }++ function updateLinting(cm, annotationsNotSorted) {+ clearMarks(cm);+ var state = cm.state.lint, options = state.options;++ var annotations = groupByLine(annotationsNotSorted);++ for (var line = 0; line < annotations.length; ++line) {+ var anns = annotations[line];+ if (!anns) continue;++ var maxSeverity = null;+ var tipLabel = state.hasGutter && document.createDocumentFragment();++ for (var i = 0; i < anns.length; ++i) {+ var ann = anns[i];+ var severity = ann.severity;+ if (!SEVERITIES.test(severity)) severity = "error";+ maxSeverity = getMaxSeverity(maxSeverity, severity);++ if (options.formatAnnotation) ann = options.formatAnnotation(ann);+ if (state.hasGutter) tipLabel.appendChild(annotationTooltip(ann));++ if (ann.to) state.marked.push(cm.markText(ann.from, ann.to, {+ className: "CodeMirror-lint-mark-" + severity,+ __annotation: ann+ }));+ }++ if (state.hasGutter)+ cm.setGutterMarker(line, GUTTER_ID, makeMarker(tipLabel, maxSeverity, anns.length > 1,+ state.options.tooltips));+ }+ if (options.onUpdateLinting) options.onUpdateLinting(annotationsNotSorted, annotations, cm);+ }++ function onChange(cm) {+ var state = cm.state.lint;+ clearTimeout(state.timeout);+ state.timeout = setTimeout(function(){startLinting(cm);}, state.options.delay || 500);+ }++ function popupSpanTooltip(ann, e) {+ var target = e.target || e.srcElement;+ showTooltipFor(e, annotationTooltip(ann), target);+ }++ // When the mouseover fires, the cursor might not actually be over+ // the character itself yet. These pairs of x,y offsets are used to+ // probe a few nearby points when no suitable marked range is found.+ var nearby = [0, 0, 0, 5, 0, -5, 5, 0, -5, 0];++ function onMouseOver(cm, e) {+ if (!/\bCodeMirror-lint-mark-/.test((e.target || e.srcElement).className)) return;+ for (var i = 0; i < nearby.length; i += 2) {+ var spans = cm.findMarksAt(cm.coordsChar({left: e.clientX + nearby[i],+ top: e.clientY + nearby[i + 1]}));+ for (var j = 0; j < spans.length; ++j) {+ var span = spans[j], ann = span.__annotation;+ if (ann) return popupSpanTooltip(ann, e);+ }+ }+ }++ function optionHandler(cm, val, old) {+ if (old && old != CodeMirror.Init) {+ clearMarks(cm);+ cm.off("change", onChange);+ CodeMirror.off(cm.getWrapperElement(), "mouseover", cm.state.lint.onMouseOver);+ delete cm.state.lint;+ }++ if (val) {+ var gutters = cm.getOption("gutters"), hasLintGutter = false;+ for (var i = 0; i < gutters.length; ++i) if (gutters[i] == GUTTER_ID) hasLintGutter = true;+ var state = cm.state.lint = new LintState(cm, parseOptions(cm, val), hasLintGutter);+ cm.on("change", onChange);+ if (state.options.tooltips != false)+ CodeMirror.on(cm.getWrapperElement(), "mouseover", state.onMouseOver);++ startLinting(cm);+ }+ }++ CodeMirror.defineOption("lintWith", false, optionHandler); // deprecated+ CodeMirror.defineOption("lint", false, optionHandler); // deprecated+})();++var parsecWidgetCounter = 0;++// Register the comm target.+var ParsecWidget = function (comm) {+ this.comm = comm;+ this.comm.on_msg($.proxy(this.handler, this));++ // Get the cell that was probably executed.+ // The msg_id:cell mapping will make this possible without guessing.+ this.cell = IPython.notebook.get_cell(IPython.notebook.get_selected_index()-1);++ // Store this widget so we can use it from callbacks.+ var widget = this;++ // Editor options.+ var options = {+ lineNumbers: true,+ // Show parsec errors as lint errors.+ gutters: ["CodeMirror-lint-markers"],+ lintWith: {+ "getAnnotations": function(cm, update, opts) {+ var errs = [];+ if (widget.hasError) {+ var col = widget.error["col"];+ var line = widget.error["line"];+ errs = [{+ from: CodeMirror.Pos(line - 1, col - 1),+ to: CodeMirror.Pos(line - 1, col),+ message: widget.error["msg"],+ severity: "error"+ }];+ }+ update(cm, errs);+ },+ "async": true,+ }+ };++ // Create the editor.+ var out = this.cell.output_area.element;+ this.textarea = out.find("#parsec-editor")[0];+ this.output = out.find("#parsec-output")[0];+ // Give the elements a different name.+ this.textarea.id += parsecWidgetCounter;+ this.output.id += parsecWidgetCounter;+ parsecWidgetCounter++;++ var editor = CodeMirror.fromTextArea(this.textarea, options);+ var editor = editor;++ // Update every key press.+ editor.on("keyup", function() {+ var text = editor.getDoc().getValue();+ comm.send({"text": text});+ });+};++ParsecWidget.prototype.handler = function(msg) {+ var data = msg.content.data;+ this.hasError = (data["status"] == "error");+ console.log(this.hasError);+ if (this.hasError) {+ this.output.innerHTML = data["msg"];+ this.error = data;+ } else {+ this.output.innerHTML = data["result"];+ }+};++// Register this widget.+IPython.notebook.kernel.comm_manager.register_target('parsec', IPython.utils.always_new(ParsecWidget));+console.log("Registering Parsec widget.");+}