mirror of
https://github.com/renbaoshuo/S2OJ.git
synced 2024-11-27 00:56:20 +00:00
96d4a3ecf7
Due to historical reasons, the code is in subfolder "1". With SVN removal, we place the code back and remove the annoying "1" folder.
210 lines
7.0 KiB
JavaScript
210 lines
7.0 KiB
JavaScript
// CodeMirror, copyright (c) by Marijn Haverbeke and others
|
|
// Distributed under an MIT license: http://codemirror.net/LICENSE
|
|
|
|
(function(mod) {
|
|
if (typeof exports == "object" && typeof module == "object") // CommonJS
|
|
mod(require("../../lib/codemirror"));
|
|
else if (typeof define == "function" && define.amd) // AMD
|
|
define(["../../lib/codemirror"], mod);
|
|
else // Plain browser env
|
|
mod(CodeMirror);
|
|
})(function(CodeMirror) {
|
|
"use strict";
|
|
var GUTTER_ID = "CodeMirror-lint-markers";
|
|
|
|
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 (!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 (!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]}, "client"));
|
|
for (var j = 0; j < spans.length; ++j) {
|
|
var span = spans[j], ann = span.__annotation;
|
|
if (ann) return popupSpanTooltip(ann, e);
|
|
}
|
|
}
|
|
}
|
|
|
|
CodeMirror.defineOption("lint", false, function(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);
|
|
}
|
|
});
|
|
});
|