settingeditor.css 1.6 KB

12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576
  1. /*-----------------------------------------------------------------------------
  2. | Copyright (c) Jupyter Development Team.
  3. | Distributed under the terms of the Modified BSD License.
  4. |----------------------------------------------------------------------------*/
  5. #setting-editor.jp-SettingEditor {
  6. background-color: var(--md-grey-200);
  7. outline: none;
  8. }
  9. #setting-editor.jp-SettingEditor ul.jp-PluginList {
  10. background-color: var(--md-grey-300);
  11. color: var(--jp-ui-font-color1);
  12. font-size: var(--jp-ui-font-size1);
  13. list-style-type: none;
  14. margin: 0;
  15. padding: 0;
  16. }
  17. #setting-editor.jp-SettingEditor ul.jp-PluginList li {
  18. padding: 2px 0 5px 5px;
  19. }
  20. #setting-editor.jp-SettingEditor ul.jp-PluginList li:hover {
  21. background-color: var(--md-grey-200);
  22. }
  23. #setting-editor.jp-SettingEditor ul.jp-PluginList li.jp-mod-selected {
  24. background-color: var(--md-grey-200);
  25. }
  26. #setting-editor.jp-SettingEditor .jp-PluginList-icon {
  27. display: inline-block;
  28. height: 20px;
  29. width: 20px;
  30. margin-right: 3px;
  31. position: relative;
  32. top: 3px;
  33. }
  34. #setting-editor.jp-SettingEditor .jp-PluginEditor {
  35. padding: 10px;
  36. }
  37. #setting-editor.jp-SettingEditor .jp-PluginEditor .jp-JSONEditor-host {
  38. height: 100%;
  39. margin-left: 0;
  40. margin-right: 0;
  41. }
  42. #setting-editor.jp-SettingEditor .jp-PluginEditor .jp-JSONEditor-header {
  43. height: 20px;
  44. }
  45. #setting-editor.jp-SettingEditor .jp-PluginEditor .jp-PluginFieldset {
  46. border: 1px solid var(--jp-brand-color1);
  47. margin: 0;
  48. padding: 0;
  49. }
  50. #setting-editor.jp-SettingEditor .jp-PluginEditor .jp-PluginFieldset legend {
  51. color: var(--jp-brand-color1);
  52. font-size: 80%;
  53. font-weight: bold;
  54. margin-left: 10px;
  55. }