##// 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
618 lines | 14.6 KiB | text/html | HtmlLexer
<!doctype html>
<html>
<head>
<title>CodeMirror: LESS mode</title>
<link rel="stylesheet" href="../../lib/codemirror.css">
<script src="../../lib/codemirror.js"></script>
<script src="less.js"></script>
<style>.CodeMirror {background: #f8f8f8; border: 1px solid #ddd; font-size:12px} .CodeMirror-scroll {height: 400px}</style>
<link rel="stylesheet" href="../../doc/docs.css">
<link rel="stylesheet" href="../../theme/lesser-dark.css">
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
</head>
<body>
<h1>CodeMirror: LESS mode</h1>
<form><textarea id="code" name="code">/* Some LESS code */
button {
width: 32px;
height: 32px;
border: 0;
margin: 4px;
cursor: pointer;
}
button.icon-plus { background: url(http://dahlström.net/tmp/sharp-icons/svg-icon-target.svg#plus) no-repeat; }
button.icon-chart { background: url(http://dahlström.net/tmp/sharp-icons/svg-icon-target.svg#chart) no-repeat; }
button:hover { background-color: #999; }
button:active { background-color: #666; }
@test_a: #eeeQQQ;//this is not a valid hex value and thus parsed as an element id
@test_b: #eeeFFF //this is a valid hex value but the declaration doesn't end with a semicolon and thus parsed as an element id
#eee aaa .box
{
#test bbb {
width: 500px;
height: 250px;
background-image: url(dir/output/sheep.png), url( betweengrassandsky.png );
background-position: center bottom, left top;
background-repeat: no-repeat;
}
}
@base: #f938ab;
.box-shadow(@style, @c) when (iscolor(@c)) {
box-shadow: @style @c;
-webkit-box-shadow: @style @c;
-moz-box-shadow: @style @c;
}
.box-shadow(@style, @alpha: 50%) when (isnumber(@alpha)) {
.box-shadow(@style, rgba(0, 0, 0, @alpha));
}
@color: #4D926F;
#header {
color: @color;
color: #000000;
}
h2 {
color: @color;
}
.rounded-corners (@radius: 5px) {
border-radius: @radius;
-webkit-border-radius: @radius;
-moz-border-radius: @radius;
}
#header {
.rounded-corners;
}
#footer {
.rounded-corners(10px);
}
.box-shadow (@x: 0, @y: 0, @blur: 1px, @alpha) {
@val: @x @y @blur rgba(0, 0, 0, @alpha);
box-shadow: @val;
-webkit-box-shadow: @val;
-moz-box-shadow: @val;
}
.box { @base: #f938ab;
color: saturate(@base, 5%);
border-color: lighten(@base, 30%);
div { .box-shadow(0, 0, 5px, 0.4) }
}
@import url("something.css");
@light-blue: hsl(190, 50%, 65%);
@light-yellow: desaturate(#fefec8, 10%);
@dark-yellow: desaturate(darken(@light-yellow, 10%), 40%);
@darkest: hsl(20, 0%, 15%);
@dark: hsl(190, 20%, 30%);
@medium: hsl(10, 60%, 30%);
@light: hsl(90, 40%, 20%);
@lightest: hsl(90, 20%, 90%);
@highlight: hsl(80, 50%, 90%);
@blue: hsl(210, 60%, 20%);
@alpha-blue: hsla(210, 60%, 40%, 0.5);
.box-shadow (@x, @y, @blur, @alpha) {
@value: @x @y @blur rgba(0, 0, 0, @alpha);
box-shadow: @value;
-moz-box-shadow: @value;
-webkit-box-shadow: @value;
}
.border-radius (@radius) {
border-radius: @radius;
-moz-border-radius: @radius;
-webkit-border-radius: @radius;
}
.border-radius (@radius, bottom) {
border-top-right-radius: 0;
border-top-left-radius: 0;
-moz-border-top-right-radius: 0;
-moz-border-top-left-radius: 0;
-webkit-border-top-left-radius: 0;
-webkit-border-top-right-radius: 0;
}
.border-radius (@radius, right) {
border-bottom-left-radius: 0;
border-top-left-radius: 0;
-moz-border-bottom-left-radius: 0;
-moz-border-top-left-radius: 0;
-webkit-border-bottom-left-radius: 0;
-webkit-border-top-left-radius: 0;
}
.box-shadow-inset (@x, @y, @blur, @color) {
box-shadow: @x @y @blur @color inset;
-moz-box-shadow: @x @y @blur @color inset;
-webkit-box-shadow: @x @y @blur @color inset;
}
.code () {
font-family: 'Bitstream Vera Sans Mono',
'DejaVu Sans Mono',
'Monaco',
Courier,
monospace !important;
}
.wrap () {
text-wrap: wrap;
white-space: pre-wrap; /* css-3 */
white-space: -moz-pre-wrap; /* Mozilla, since 1999 */
white-space: -pre-wrap; /* Opera 4-6 */
white-space: -o-pre-wrap; /* Opera 7 */
word-wrap: break-word; /* Internet Explorer 5.5+ */
}
html { margin: 0 }
body {
background-color: @darkest;
margin: 0 auto;
font-family: Arial, sans-serif;
font-size: 100%;
overflow-x: hidden;
}
nav, header, footer, section, article {
display: block;
}
a {
color: #b83000;
}
h1 a {
color: black;
text-decoration: none;
}
a:hover {
text-decoration: underline;
}
h1, h2, h3, h4 {
margin: 0;
font-weight: normal;
}
ul, li {
list-style-type: none;
}
code { .code; }
code {
.string, .regexp { color: @dark }
.keyword { font-weight: bold }
.comment { color: rgba(0, 0, 0, 0.5) }
.number { color: @blue }
.class, .special { color: rgba(0, 50, 100, 0.8) }
}
pre {
padding: 0 30px;
.wrap;
}
blockquote {
font-style: italic;
}
body > footer {
text-align: left;
margin-left: 10px;
font-style: italic;
font-size: 18px;
color: #888;
}
#logo {
margin-top: 30px;
margin-bottom: 30px;
display: block;
width: 199px;
height: 81px;
background: url(/images/logo.png) no-repeat;
}
nav {
margin-left: 15px;
}
nav a, #dropdown li {
display: inline-block;
color: white;
line-height: 42px;
margin: 0;
padding: 0px 15px;
text-shadow: -1px -1px 1px rgba(0, 0, 0, 0.5);
text-decoration: none;
border: 2px solid transparent;
border-width: 0 2px;
&:hover {
.dark-red;
text-decoration: none;
}
}
.dark-red {
@red: @medium;
border: 2px solid darken(@red, 25%);
border-left-color: darken(@red, 15%);
border-right-color: darken(@red, 15%);
border-bottom: 0;
border-top: 0;
background-color: darken(@red, 10%);
}
.content {
margin: 0 auto;
width: 980px;
}
#menu {
position: absolute;
width: 100%;
z-index: 3;
clear: both;
display: block;
background-color: @blue;
height: 42px;
border-top: 2px solid lighten(@alpha-blue, 20%);
border-bottom: 2px solid darken(@alpha-blue, 25%);
.box-shadow(0, 1px, 8px, 0.6);
-moz-box-shadow: 0 0 0 #000; // Because firefox sucks.
&.docked {
background-color: hsla(210, 60%, 40%, 0.4);
}
&:hover {
background-color: @blue;
}
#dropdown {
margin: 0 0 0 117px;
padding: 0;
padding-top: 5px;
display: none;
width: 190px;
border-top: 2px solid @medium;
color: @highlight;
border: 2px solid darken(@medium, 25%);
border-left-color: darken(@medium, 15%);
border-right-color: darken(@medium, 15%);
border-top-width: 0;
background-color: darken(@medium, 10%);
ul {
padding: 0px;
}
li {
font-size: 14px;
display: block;
text-align: left;
padding: 0;
border: 0;
a {
display: block;
padding: 0px 15px;
text-decoration: none;
color: white;
&:hover {
background-color: darken(@medium, 15%);
text-decoration: none;
}
}
}
.border-radius(5px, bottom);
.box-shadow(0, 6px, 8px, 0.5);
}
}
#main {
margin: 0 auto;
width: 100%;
background-color: @light-blue;
border-top: 8px solid darken(@light-blue, 5%);
#intro {
background-color: lighten(@light-blue, 25%);
float: left;
margin-top: -8px;
margin-right: 5px;
height: 380px;
position: relative;
z-index: 2;
font-family: 'Droid Serif', 'Georgia';
width: 395px;
padding: 45px 20px 23px 30px;
border: 2px dashed darken(@light-blue, 10%);
.box-shadow(1px, 0px, 6px, 0.5);
border-bottom: 0;
border-top: 0;
#download { color: transparent; border: 0; float: left; display: inline-block; margin: 15px 0 15px -5px; }
#download img { display: inline-block}
#download-info {
code {
font-size: 13px;
}
color: @blue + #333; display: inline; float: left; margin: 36px 0 0 15px }
}
h2 {
span {
color: @medium;
}
color: @blue;
margin: 20px 0;
font-size: 24px;
line-height: 1.2em;
}
h3 {
color: @blue;
line-height: 1.4em;
margin: 30px 0 15px 0;
font-size: 1em;
text-shadow: 0px 0px 0px @lightest;
span { color: @medium }
}
#example {
p {
font-size: 18px;
color: @blue;
font-weight: bold;
text-shadow: 0px 1px 1px @lightest;
}
pre {
margin: 0;
text-shadow: 0 -1px 1px @darkest;
margin-top: 20px;
background-color: desaturate(@darkest, 8%);
border: 0;
width: 450px;
color: lighten(@lightest, 2%);
background-repeat: repeat;
padding: 15px;
border: 1px dashed @lightest;
line-height: 15px;
.box-shadow(0, 0px, 15px, 0.5);
.code;
.border-radius(2px);
code .attribute { color: hsl(40, 50%, 70%) }
code .variable { color: hsl(120, 10%, 50%) }
code .element { color: hsl(170, 20%, 50%) }
code .string, .regexp { color: hsl(75, 50%, 65%) }
code .class { color: hsl(40, 40%, 60%); font-weight: normal }
code .id { color: hsl(50, 40%, 60%); font-weight: normal }
code .comment { color: rgba(255, 255, 255, 0.2) }
code .number, .color { color: hsl(10, 40%, 50%) }
code .class, code .mixin, .special { color: hsl(190, 20%, 50%) }
#time { color: #aaa }
}
float: right;
font-size: 12px;
margin: 0;
margin-top: 15px;
padding: 0;
width: 500px;
}
}
.page {
.content {
width: 870px;
padding: 45px;
}
margin: 0 auto;
font-family: 'Georgia', serif;
font-size: 18px;
line-height: 26px;
padding: 0 60px;
code {
font-size: 16px;
}
pre {
border-width: 1px;
border-style: dashed;
padding: 15px;
margin: 15px 0;
}
h1 {
text-align: left;
font-size: 40px;
margin-top: 15px;
margin-bottom: 35px;
}
p + h1 { margin-top: 60px }
h2, h3 {
margin: 30px 0 15px 0;
}
p + h2, pre + h2, code + h2 {
border-top: 6px solid rgba(255, 255, 255, 0.1);
padding-top: 30px;
}
h3 {
margin: 15px 0;
}
}
#docs {
@bg: lighten(@light-blue, 5%);
border-top: 2px solid lighten(@bg, 5%);
color: @blue;
background-color: @light-blue;
.box-shadow(0, -2px, 5px, 0.2);
h1 {
font-family: 'Droid Serif', 'Georgia', serif;
padding-top: 30px;
padding-left: 45px;
font-size: 44px;
text-align: left;
margin: 30px 0 !important;
text-shadow: 0px 1px 1px @lightest;
font-weight: bold;
}
.content {
clear: both;
border-color: transparent;
background-color: lighten(@light-blue, 25%);
.box-shadow(0, 5px, 5px, 0.4);
}
pre {
@background: lighten(@bg, 30%);
color: lighten(@blue, 10%);
background-color: @background;
border-color: lighten(@light-blue, 25%);
border-width: 2px;
code .attribute { color: hsl(40, 50%, 30%) }
code .variable { color: hsl(120, 10%, 30%) }
code .element { color: hsl(170, 20%, 30%) }
code .string, .regexp { color: hsl(75, 50%, 35%) }
code .class { color: hsl(40, 40%, 30%); font-weight: normal }
code .id { color: hsl(50, 40%, 30%); font-weight: normal }
code .comment { color: rgba(0, 0, 0, 0.4) }
code .number, .color { color: hsl(10, 40%, 30%) }
code .class, code .mixin, .special { color: hsl(190, 20%, 30%) }
}
pre code { font-size: 15px }
p + h2, pre + h2, code + h2 { border-top-color: rgba(0, 0, 0, 0.1) }
}
td {
padding-right: 30px;
}
#synopsis {
.box-shadow(0, 5px, 5px, 0.2);
}
#synopsis, #about {
h2 {
font-size: 30px;
padding: 10px 0;
}
h1 + h2 {
margin-top: 15px;
}
h3 { font-size: 22px }
.code-example {
border-spacing: 0;
border-width: 1px;
border-style: dashed;
padding: 0;
pre { border: 0; margin: 0 }
td {
border: 0;
margin: 0;
background-color: desaturate(darken(@darkest, 5%), 20%);
vertical-align: top;
padding: 0;
}
tr { padding: 0 }
}
.css-output {
td {
border-left: 0;
}
}
.less-example {
//border-right: 1px dotted rgba(255, 255, 255, 0.5) !important;
}
.css-output, .less-example {
width: 390px;
}
pre {
padding: 20px;
line-height: 20px;
font-size: 14px;
}
}
#about, #synopsis, #guide {
a {
text-decoration: none;
color: @light-yellow;
border-bottom: 1px dashed rgba(255, 255, 255, 0.2);
&:hover {
text-decoration: none;
border-bottom: 1px dashed @light-yellow;
}
}
@bg: desaturate(darken(@darkest, 5%), 20%);
text-shadow: 0 -1px 1px lighten(@bg, 5%);
color: @highlight;
background-color: @bg;
.content {
background-color: desaturate(@darkest, 20%);
clear: both;
.box-shadow(0, 5px, 5px, 0.4);
}
h1, h2, h3 {
color: @dark-yellow;
}
pre {
code .attribute { color: hsl(40, 50%, 70%) }
code .variable { color: hsl(120, 10%, 50%) }
code .element { color: hsl(170, 20%, 50%) }
code .string, .regexp { color: hsl(75, 50%, 65%) }
code .class { color: hsl(40, 40%, 60%); font-weight: normal }
code .id { color: hsl(50, 40%, 60%); font-weight: normal }
code .comment { color: rgba(255, 255, 255, 0.2) }
code .number, .color { color: hsl(10, 40%, 50%) }
code .class, code .mixin, .special { color: hsl(190, 20%, 50%) }
background-color: @bg;
border-color: darken(@light-yellow, 5%);
}
code {
color: darken(@dark-yellow, 5%);
.string, .regexp { color: desaturate(@light-blue, 15%) }
.keyword { color: hsl(40, 40%, 60%); font-weight: normal }
.comment { color: rgba(255, 255, 255, 0.2) }
.number { color: lighten(@blue, 10%) }
.class, .special { color: hsl(190, 20%, 50%) }
}
}
#guide {
background-color: @darkest;
.content {
background-color: transparent;
}
}
#about {
background-color: @darkest !important;
.content {
background-color: desaturate(lighten(@darkest, 3%), 5%);
}
}
#synopsis {
background-color: desaturate(lighten(@darkest, 3%), 5%) !important;
.content {
background-color: desaturate(lighten(@darkest, 3%), 5%);
}
pre {}
}
#synopsis, #guide {
.content {
.box-shadow(0, 0px, 0px, 0.0);
}
}
#about footer {
margin-top: 30px;
padding-top: 30px;
border-top: 6px solid rgba(0, 0, 0, 0.1);
text-align: center;
font-size: 16px;
color: rgba(255, 255, 255, 0.35);
#copy { font-size: 12px }
text-shadow: -1px -1px 1px rgba(0, 0, 0, 0.02);
}
</textarea></form>
<script>
var editor = CodeMirror.fromTextArea(document.getElementById("code"), {
theme: "lesser-dark",
lineNumbers : true,
matchBrackets : true
});
</script>
<p><strong>MIME types defined:</strong> <code>text/x-less</code>, <code>text/css</code> (if not previously defined).</p>
</body>
</html>