settingeditor.css 2.9 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136
  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 .p-SplitPanel-handle {
  10. background-color: var(--md-grey-400);
  11. }
  12. #setting-editor.jp-SettingEditor .jp-SettingEditorInstructions {
  13. text-align: center;
  14. }
  15. #setting-editor.jp-SettingEditor .jp-SettingEditorInstructions-icon {
  16. display: inline-block;
  17. background-size: 60px;
  18. width: 60px;
  19. height: 78px;
  20. margin-right: 5px;
  21. }
  22. #setting-editor.jp-SettingEditor .jp-SettingEditorInstructions-title {
  23. font-size: 32px;
  24. font-weight: 200;
  25. line-height: 78px;
  26. vertical-align: top;
  27. }
  28. #setting-editor.jp-SettingEditor .jp-SettingEditorInstructions-text {
  29. font-size: var(--jp-ui-font-size2);
  30. }
  31. #setting-editor.jp-SettingEditor ul.jp-PluginList {
  32. background-color: var(--jp-layout-color0);
  33. color: var(--jp-ui-font-color1);
  34. font-size: var(--jp-ui-font-size1);
  35. list-style-type: none;
  36. margin: 0;
  37. padding: 0;
  38. min-width: 150px;
  39. width: 150px;
  40. }
  41. #setting-editor.jp-SettingEditor ul.jp-PluginList li {
  42. border: 1px solid transparent;
  43. overflow: hidden;
  44. padding: 2px 0 5px 5px;
  45. text-overflow: ellipsis;
  46. white-space: nowrap;
  47. }
  48. #setting-editor.jp-SettingEditor ul.jp-PluginList li:hover {
  49. border: 1px solid var(--md-grey-300);
  50. background-color: var(--md-grey-200);
  51. }
  52. #setting-editor.jp-SettingEditor ul.jp-PluginList li.jp-mod-selected {
  53. background-color: var(--md-grey-200);
  54. }
  55. #setting-editor.jp-SettingEditor .jp-PluginList-icon {
  56. display: inline-block;
  57. height: 20px;
  58. width: 20px;
  59. margin-right: 3px;
  60. position: relative;
  61. top: 3px;
  62. }
  63. #setting-editor.jp-SettingEditor .jp-PluginEditor {
  64. padding: 10px;
  65. }
  66. #setting-editor.jp-SettingEditor .jp-PluginEditor .jp-JSONEditor-host {
  67. height: 100%;
  68. margin-left: 0;
  69. margin-right: 0;
  70. }
  71. #setting-editor.jp-SettingEditor .jp-PluginEditor .jp-JSONEditor-header {
  72. position: absolute;
  73. right: 0;
  74. z-index: 9999;
  75. }
  76. #setting-editor.jp-SettingEditor .jp-PluginEditor .jp-PluginFieldset {
  77. border: 1px solid var(--jp-brand-color1);
  78. margin: 0;
  79. padding: 0;
  80. }
  81. #setting-editor.jp-SettingEditor .jp-PluginEditor .jp-PluginFieldset legend {
  82. color: var(--jp-brand-color1);
  83. font-size: 70%;
  84. font-weight: bold;
  85. margin-left: 15px;
  86. }
  87. #setting-editor.jp-SettingEditor .jp-PluginEditor .jp-PluginFieldset ul {
  88. color: var(--jp-ui-font-color1);
  89. font-size: var(--jp-ui-font-size1);
  90. list-style-type: none;
  91. margin: 0;
  92. padding: 0;
  93. }
  94. #setting-editor.jp-SettingEditor .jp-PluginEditor .jp-PluginFieldset li {
  95. background-color: var(--md-grey-400);
  96. color: var(--jp-ui-font-color2);
  97. display: inline-block;
  98. margin: 3px;
  99. padding: 3px;
  100. }