Turn on soft wrap for editor
Some cleanup
@@ -134,24 +134,21 @@ class LiveEditPage(Page):
}
.container iframe {
- flex: 5 1 auto;
- }
- .container div {
flex: 1 1 auto;
}
+ .container #editor {
+ flex: 2 1 auto;
+ }
nav {
display: none;
}
'''
),
- parts__result=html.iframe(attrs__id='result', attrs__style=dict(width='100%', height='400px')),
+ parts__result=html.iframe(attrs__id='result'),
parts__editor=html.div(
ast_of_old_code.get_code(),
- attrs=dict(
- style__height='500px',
- id='editor',
- ),
+ attrs__id='editor',
),
parts__script=html.script(mark_safe('''
@@ -181,6 +178,7 @@ class LiveEditPage(Page):
});
let foo = await response.json();
if (foo.page) {
+ // TODO: get scroll position and restore it
document.getElementById('result').srcdoc = foo.page;
}
}
@@ -192,6 +190,7 @@ class LiveEditPage(Page):
editor.session.on('change', foo);
editor.setFontSize(14);
+ editor.session.setUseWrapMode(true);
foo();
''')),
