##// END OF EJS Templates
Merge pull request #2389 from takluyver/catch-histdb-errors...
Merge pull request #2389 from takluyver/catch-histdb-errors Catch sqlite DatabaseErrors in more places when reading the history database It seems sqlite can encounter corruption and throw an error when reading the database, although it has connected successfully. This borrows the move-and-recreate machinery we already had on connecting to the database. If such an error occurs, the corrupted file is moved and the user get warned of the name of the corrupted file.

File last commit:

r8053:58574fbf
r8503:7904325b merge
Show More
index.html
104 lines | 4.0 KiB | text/html | HtmlLexer
<!doctype html>
<html>
<head>
<title>CodeMirror: Diff mode</title>
<link rel="stylesheet" href="../../lib/codemirror.css">
<script src="../../lib/codemirror.js"></script>
<script src="diff.js"></script>
<style>
.CodeMirror {border-top: 1px solid #ddd; border-bottom: 1px solid #ddd;}
span.cm-meta {color: #a0b !important;}
span.cm-error { background-color: black; opacity: 0.4;}
span.cm-error.cm-string { background-color: red; }
span.cm-error.cm-tag { background-color: #2b2; }
</style>
<link rel="stylesheet" href="../../doc/docs.css">
</head>
<body>
<h1>CodeMirror: Diff mode</h1>
<form><textarea id="code" name="code">
diff --git a/index.html b/index.html
index c1d9156..7764744 100644
--- a/index.html
+++ b/index.html
@@ -95,7 +95,8 @@ StringStream.prototype = {
<script>
var editor = CodeMirror.fromTextArea(document.getElementById("code"), {
lineNumbers: true,
- autoMatchBrackets: true
+ autoMatchBrackets: true,
+ onGutterClick: function(x){console.log(x);}
});
</script>
</body>
diff --git a/lib/codemirror.js b/lib/codemirror.js
index 04646a9..9a39cc7 100644
--- a/lib/codemirror.js
+++ b/lib/codemirror.js
@@ -399,10 +399,16 @@ var CodeMirror = (function() {
}
function onMouseDown(e) {
- var start = posFromMouse(e), last = start;
+ var start = posFromMouse(e), last = start, target = e.target();
if (!start) return;
setCursor(start.line, start.ch, false);
if (e.button() != 1) return;
+ if (target.parentNode == gutter) {
+ if (options.onGutterClick)
+ options.onGutterClick(indexOf(gutter.childNodes, target) + showingFrom);
+ return;
+ }
+
if (!focused) onFocus();
e.stop();
@@ -808,7 +814,7 @@ var CodeMirror = (function() {
for (var i = showingFrom; i < showingTo; ++i) {
var marker = lines[i].gutterMarker;
if (marker) html.push('<div class="' + marker.style + '">' + htmlEscape(marker.text) + '</div>');
- else html.push("<div>" + (options.lineNumbers ? i + 1 : "\u00a0") + "</div>");
+ else html.push("<div>" + (options.lineNumbers ? i + options.firstLineNumber : "\u00a0") + "</div>");
}
gutter.style.display = "none"; // TODO test whether this actually helps
gutter.innerHTML = html.join("");
@@ -1371,10 +1377,8 @@ var CodeMirror = (function() {
if (option == "parser") setParser(value);
else if (option === "lineNumbers") setLineNumbers(value);
else if (option === "gutter") setGutter(value);
- else if (option === "readOnly") options.readOnly = value;
- else if (option === "indentUnit") {options.indentUnit = indentUnit = value; setParser(options.parser);}
- else if (/^(?:enterMode|tabMode|indentWithTabs|readOnly|autoMatchBrackets|undoDepth)$/.test(option)) options[option] = value;
- else throw new Error("Can't set option " + option);
+ else if (option === "indentUnit") {options.indentUnit = value; setParser(options.parser);}
+ else options[option] = value;
},
cursorCoords: cursorCoords,
undo: operation(undo),
@@ -1402,7 +1406,8 @@ var CodeMirror = (function() {
replaceRange: operation(replaceRange),
operation: function(f){return operation(f)();},
- refresh: function(){updateDisplay([{from: 0, to: lines.length}]);}
+ refresh: function(){updateDisplay([{from: 0, to: lines.length}]);},
+ getInputField: function(){return input;}
};
return instance;
}
@@ -1420,6 +1425,7 @@ var CodeMirror = (function() {
readOnly: false,
onChange: null,
onCursorActivity: null,
+ onGutterClick: null,
autoMatchBrackets: false,
workTime: 200,
workDelay: 300,
</textarea></form>
<script>
var editor = CodeMirror.fromTextArea(document.getElementById("code"), {});
</script>
<p><strong>MIME types defined:</strong> <code>text/x-diff</code>.</p>
</body>
</html>