settingeditor.css 4.8 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237
  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. overflow: auto;
  92. }
  93. #setting-editor .jp-PluginEditor .jp-JSONEditor-header {
  94. position: absolute;
  95. right: 0;
  96. z-index: 9999;
  97. }
  98. #setting-editor .jp-PluginEditor .jp-PluginFieldset {
  99. border: 1px solid var(--jp-brand-color1);
  100. margin: 0;
  101. overflow-y: auto;
  102. padding: 0;
  103. }
  104. #setting-editor .jp-PluginEditor .jp-PluginFieldset legend {
  105. color: var(--jp-brand-color1);
  106. font-size: 70%;
  107. font-weight: bold;
  108. margin-left: 15px;
  109. }
  110. #setting-editor .jp-PluginEditor table.jp-PluginFieldset-table {
  111. table-layout: fixed;
  112. color: var(--jp-ui-font-color1);
  113. font-size: var(--jp-ui-font-size1);
  114. padding: 2px;
  115. width: calc(100% - 4px);
  116. overflow: hidden;
  117. }
  118. #setting-editor .jp-PluginEditor tr {
  119. color: var(--jp-ui-font-color2);
  120. height: var( --jp-private-settingeditor-row-height);
  121. overflow: hidden;
  122. }
  123. #setting-editor .jp-PluginEditor th {
  124. background-color: var(--jp-layout-color3);
  125. border: 1px solid transparent;
  126. font-weight: bold;
  127. height: var( --jp-private-settingeditor-row-height);
  128. }
  129. #setting-editor .jp-PluginEditor td {
  130. border: 1px solid transparent;
  131. height: var( --jp-private-settingeditor-row-height);
  132. }
  133. #setting-editor .jp-PluginEditor th.jp-PluginFieldset-add {
  134. width: var(--jp-private-settingeditor-add-width);
  135. }
  136. #setting-editor .jp-PluginEditor th.jp-PluginFieldset-key {
  137. width: var(--jp-private-settingeditor-key-width);
  138. }
  139. #setting-editor .jp-PluginEditor th.jp-PluginFieldset-type {
  140. width: var(--jp-private-settingeditor-type-width);
  141. }
  142. #setting-editor .jp-PluginEditor td.jp-PluginFieldset-add {
  143. cursor: pointer;
  144. text-align: center;
  145. }
  146. #setting-editor .jp-PluginEditor td.jp-PluginFieldset-add.jp-mod-active:hover {
  147. border: 1px solid var(--jp-toolbar-border-color);
  148. }
  149. #setting-editor .jp-PluginEditor td.jp-PluginFieldset-key {
  150. overflow: hidden;
  151. white-space: nowrap;
  152. text-overflow: ellipsis;
  153. }
  154. #setting-editor .jp-PluginEditor td.jp-PluginFieldset-value {
  155. overflow: hidden;
  156. white-space: nowrap;
  157. text-overflow: ellipsis;
  158. }
  159. #setting-editor .jp-PluginEditor td.jp-PluginFieldset-type {
  160. text-align: right;
  161. }
  162. #setting-editor .jp-PluginEditor .jp-PluginFieldset-button {
  163. display: inline-block;
  164. background-position: center;
  165. background-repeat: no-repeat;
  166. background-size: 8px;
  167. border: 1px solid var(--jp-layout-color3);
  168. border-radius: 8px;
  169. width: 8px;
  170. height: 8px;
  171. margin-top: 3px;
  172. }