blob: 056fe628a4e516871531c2d3d31b63b70d46a523 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
{
// Text Editor
// @jupyterlab/fileeditor-extension:plugin
// Text editor settings.
// ***************************************
// Editor Configuration
// The configuration for all text editors; it will override the CodeMirror default configuration.
// If `fontFamily`, `fontSize` or `lineHeight` are `null`,
// values from current theme are used.
"editorConfig": {
"customStyles": {
"fontFamily": null,
"fontSize": 16,
"lineHeight": null
},
"theme": "jupyter"
},
// Scroll behavior
// Whether to scroll past the end of text document.
"scrollPastEnd": true,
// Text editor toolbar items
// Note: To disable a toolbar item,
// copy it to User Preferences and add the
// "disabled" key. Toolbar description:
"toolbar": []
}
|
