settingeditor.css 4.8 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236
  1. /*-----------------------------------------------------------------------------
  2. | Copyright (c) Jupyter Development Team.
  3. | Distributed under the terms of the Modified BSD License.
  4. |----------------------------------------------------------------------------*/
  5. :root {
  6. --jp-private-settingeditor-row-height: 16px;
  7. --jp-private-settingeditor-add-width: 16px;
  8. --jp-private-settingeditor-key-width: 150px;
  9. --jp-private-settingeditor-type-width: 75px;
  10. }
  11. #setting-editor {
  12. background-color: var(--jp-layout-color0);
  13. border-top: var(--jp-border-width) solid var(--jp-border-color1);
  14. margin-top: -1px;
  15. outline: none;
  16. }
  17. #setting-editor::before {
  18. content: '';
  19. display: block;
  20. height: var(--jp-toolbar-micro-height);
  21. background: var(--jp-toolbar-background);
  22. border-bottom: 1px solid var(--jp-toolbar-border-color);
  23. box-shadow: var(--jp-toolbar-box-shadow);
  24. z-index: 10;
  25. }
  26. #setting-editor .p-SplitPanel {
  27. height: 100%;
  28. width: 100%;
  29. }
  30. #setting-editor .p-SplitPanel-handle {
  31. background-color: var(--jp-border-color1);
  32. }
  33. #setting-editor .jp-SettingEditorInstructions {
  34. text-align: center;
  35. }
  36. #setting-editor .jp-SettingEditorInstructions-icon {
  37. display: inline-block;
  38. background-size: 60px;
  39. width: 60px;
  40. height: 78px;
  41. margin-right: 5px;
  42. }
  43. #setting-editor .jp-SettingEditorInstructions-title {
  44. font-size: 32px;
  45. font-weight: 200;
  46. line-height: 78px;
  47. vertical-align: top;
  48. }
  49. #setting-editor .jp-SettingEditorInstructions-text {
  50. font-size: var(--jp-ui-font-size2);
  51. }
  52. #setting-editor ul.jp-PluginList {
  53. background-color: var(--jp-layout-color1);
  54. color: var(--jp-ui-font-color1);
  55. font-size: var(--jp-ui-font-size1);
  56. list-style-type: none;
  57. margin: 0;
  58. padding: 0;
  59. min-width: 150px;
  60. width: 150px;
  61. }
  62. #setting-editor ul.jp-PluginList li {
  63. border: 1px solid transparent;
  64. overflow: hidden;
  65. padding: 2px 0 5px 5px;
  66. text-overflow: ellipsis;
  67. white-space: nowrap;
  68. }
  69. #setting-editor ul.jp-PluginList li:hover {
  70. background-color: var(--jp-layout-color2);
  71. border: 1px solid var(--jp-border-color2);
  72. }
  73. #setting-editor ul.jp-PluginList li.jp-mod-selected {
  74. background-color: var(--jp-brand-color1);
  75. }
  76. #setting-editor .jp-PluginList-icon {
  77. display: inline-block;
  78. height: 20px;
  79. width: 20px;
  80. margin-right: 3px;
  81. position: relative;
  82. top: 3px;
  83. }
  84. #setting-editor .jp-PluginEditor {
  85. padding: 10px;
  86. }
  87. #setting-editor .jp-PluginEditor .jp-JSONEditor-host {
  88. height: 100%;
  89. margin-left: 0;
  90. margin-right: 0;
  91. }
  92. #setting-editor .jp-PluginEditor .jp-JSONEditor-header {
  93. position: absolute;
  94. right: 0;
  95. z-index: 9999;
  96. }
  97. #setting-editor .jp-PluginEditor .jp-PluginFieldset {
  98. border: 1px solid var(--jp-brand-color1);
  99. margin: 0;
  100. overflow-y: auto;
  101. padding: 0;
  102. }
  103. #setting-editor .jp-PluginEditor .jp-PluginFieldset legend {
  104. color: var(--jp-brand-color1);
  105. font-size: 70%;
  106. font-weight: bold;
  107. margin-left: 15px;
  108. }
  109. #setting-editor .jp-PluginEditor table.jp-PluginFieldset-table {
  110. table-layout: fixed;
  111. color: var(--jp-ui-font-color1);
  112. font-size: var(--jp-ui-font-size1);
  113. padding: 2px;
  114. width: calc(100% - 4px);
  115. overflow: hidden;
  116. }
  117. #setting-editor .jp-PluginEditor tr {
  118. color: var(--jp-ui-font-color2);
  119. height: var( --jp-private-settingeditor-row-height);
  120. overflow: hidden;
  121. }
  122. #setting-editor .jp-PluginEditor th {
  123. background-color: var(--jp-layout-color3);
  124. border: 1px solid transparent;
  125. font-weight: bold;
  126. height: var( --jp-private-settingeditor-row-height);
  127. }
  128. #setting-editor .jp-PluginEditor td {
  129. border: 1px solid transparent;
  130. height: var( --jp-private-settingeditor-row-height);
  131. }
  132. #setting-editor .jp-PluginEditor th.jp-PluginFieldset-add {
  133. width: var(--jp-private-settingeditor-add-width);
  134. }
  135. #setting-editor .jp-PluginEditor th.jp-PluginFieldset-key {
  136. width: var(--jp-private-settingeditor-key-width);
  137. }
  138. #setting-editor .jp-PluginEditor th.jp-PluginFieldset-type {
  139. width: var(--jp-private-settingeditor-type-width);
  140. }
  141. #setting-editor .jp-PluginEditor td.jp-PluginFieldset-add {
  142. cursor: pointer;
  143. text-align: center;
  144. }
  145. #setting-editor .jp-PluginEditor td.jp-PluginFieldset-add.jp-mod-active:hover {
  146. border: 1px solid var(--jp-toolbar-border-color);
  147. }
  148. #setting-editor .jp-PluginEditor td.jp-PluginFieldset-key {
  149. overflow: hidden;
  150. white-space: nowrap;
  151. text-overflow: ellipsis;
  152. }
  153. #setting-editor .jp-PluginEditor td.jp-PluginFieldset-value {
  154. overflow: hidden;
  155. white-space: nowrap;
  156. text-overflow: ellipsis;
  157. }
  158. #setting-editor .jp-PluginEditor td.jp-PluginFieldset-type {
  159. text-align: right;
  160. }
  161. #setting-editor .jp-PluginEditor .jp-PluginFieldset-button {
  162. display: inline-block;
  163. background-position: center;
  164. background-repeat: no-repeat;
  165. background-size: 8px;
  166. border: 1px solid var(--jp-layout-color3);
  167. border-radius: 8px;
  168. width: 8px;
  169. height: 8px;
  170. margin-top: 3px;
  171. }