r
/
p5.js-web-editor
1
0
Fork 0
Code Issues 1 Pull Requests Releases 1 Wiki Activity

fixes #715 in an extremely hacky way 🤷‍♀️, fixes another error in which when changing the font size, linting highlighting was misaligned

This commit is contained in:
Cassie Tarakajian 2018-10-10 17:40:47 -04:00
parent 19bffe58cf
commit d15e5d0da5
2 changed files with 5 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
client/modules/IDE/components/Editor.jsx
View File

@ -103,6 +103,8 @@ class Editor extends React.Component {
}
});
delete this._cm.options.lint.options.errors;
this._cm.setOption('extraKeys', {
[`${metaKey}-Enter`]: () => null,
[`Shift-${metaKey}-Enter`]: () => null,

5
client/styles/components/_editor.scss
View File

@ -35,7 +35,7 @@ pre.CodeMirror-line {
.CodeMirror-lint-marker-warning, .CodeMirror-lint-marker-error, .CodeMirror-lint-marker-multiple {
background-image: none;
width: #{48 / $base-font-size}rem;
width: #{49 / $base-font-size}rem;
position: absolute;
height: 100%;
right: 100%;
@ -56,8 +56,9 @@ pre.CodeMirror-line {
.CodeMirror-gutter-elt:not(.CodeMirror-linenumber) {
opacity: 0.3;
width: #{48 / $base-font-size}rem !important;
width: #{49 / $base-font-size}rem !important;
height: 100%;
left: 49px !important;
// background-color: rgb(255, 95, 82);
}