settingeditor.css 6.2 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286
  1. /*-----------------------------------------------------------------------------
  2. | Copyright (c) Jupyter Development Team.
  3. | Distributed under the terms of the Modified BSD License.
  4. |----------------------------------------------------------------------------*/
  5. :root {
  6. --jp-private-settingeditor-debug-height: 28px;
  7. --jp-private-settingeditor-key-width: 150px;
  8. --jp-private-settingeditor-legend-height: 16px;
  9. --jp-private-settingeditor-row-height: 16px;
  10. --jp-private-settingeditor-switcher-height: 32px;
  11. --jp-private-settingeditor-toolbar-height: 28px;
  12. --jp-private-settingeditor-type-width: 75px;
  13. }
  14. #setting-editor {
  15. min-width: 360px;
  16. min-height: 240px;
  17. background-color: var(--jp-layout-color0);
  18. margin-top: -1px;
  19. outline: none;
  20. /* This is needed so that all font sizing of children done in ems is
  21. * relative to this base size */
  22. font-size: var(--jp-ui-font-size1);
  23. }
  24. #setting-editor > .p-Widget {
  25. position: absolute;
  26. top: 0;
  27. bottom: 0;
  28. left: 0;
  29. right: 0;
  30. }
  31. #setting-editor .p-SplitPanel-handle {
  32. background-color: var(--jp-border-color2);
  33. }
  34. #setting-editor .jp-SettingEditorInstructions {
  35. text-align: center;
  36. }
  37. #setting-editor .jp-SettingEditorInstructions-icon {
  38. display: inline-block;
  39. background-size: 60px;
  40. width: 60px;
  41. height: 78px;
  42. margin-right: 5px;
  43. }
  44. #setting-editor .jp-SettingEditorInstructions-title {
  45. font-size: 32px;
  46. font-weight: 200;
  47. line-height: 78px;
  48. vertical-align: top;
  49. }
  50. #setting-editor .jp-SettingEditorInstructions-text {
  51. font-size: var(--jp-ui-font-size2);
  52. }
  53. #setting-editor .jp-PluginList {
  54. min-width: 120px;
  55. width: 120px;
  56. }
  57. #setting-editor .jp-PluginList-switcher {
  58. height: var(--jp-private-settingeditor-switcher-height);
  59. position: absolute;
  60. top: 1px;
  61. left: 0;
  62. right: 0;
  63. }
  64. #setting-editor .jp-PluginList-switcher button {
  65. background: var(--jp-layout-color2);
  66. color: var(--jp-ui-font-color2);
  67. border: 0;
  68. border-bottom: 1px solid var(--jp-ui-font-color3);
  69. margin: 0;
  70. padding: 0;
  71. height: var(--jp-private-settingeditor-switcher-height);
  72. width: 50%;
  73. }
  74. #setting-editor .jp-PluginList-switcher button:first-child {
  75. border-right: 1px solid var(--jp-ui-font-color3);
  76. }
  77. #setting-editor .jp-PluginList-switcher button:disabled {
  78. background: var(--jp-layout-color1);
  79. color: var(--jp-ui-font-color0);
  80. }
  81. #setting-editor .jp-PluginList ul {
  82. background-color: var(--jp-layout-color1);
  83. color: var(--jp-ui-font-color1);
  84. font-size: var(--jp-ui-font-size1);
  85. list-style-type: none;
  86. margin: 0;
  87. padding: 0;
  88. overflow-y: auto;
  89. position: absolute;
  90. top: var(--jp-private-settingeditor-switcher-height);
  91. bottom: 0;
  92. left: 0;
  93. right: 0;
  94. }
  95. #setting-editor .jp-PluginList li {
  96. border: 1px solid transparent;
  97. overflow: hidden;
  98. padding: 2px 0 5px 5px;
  99. text-overflow: ellipsis;
  100. white-space: nowrap;
  101. }
  102. #setting-editor .jp-PluginList li:hover {
  103. background-color: var(--jp-layout-color2);
  104. border: 1px solid var(--jp-border-color2);
  105. }
  106. #setting-editor .jp-PluginList li.jp-mod-selected {
  107. background-color: var(--jp-brand-color1);
  108. color: white;
  109. border: 1px solid var(--jp-brand-color1);
  110. }
  111. #setting-editor ul.jp-PluginList li.jp-mod-selected span.jp-PluginList-icon.jp-FileIcon {
  112. background-image: var(--jp-icon-file-selected);
  113. }
  114. #setting-editor .jp-PluginList-icon {
  115. display: inline-block;
  116. height: 20px;
  117. width: 20px;
  118. margin-right: 3px;
  119. position: relative;
  120. top: 3px;
  121. }
  122. #setting-editor .jp-SettingsRawEditor .jp-Toolbar {
  123. color: var(--jp-ui-font-color0);
  124. font-size: var(--jp-ui-font-size1);
  125. height: var(--jp-private-settingeditor-toolbar-height);
  126. max-height: var(--jp-private-settingeditor-toolbar-height);
  127. }
  128. #setting-editor .jp-SettingsRawEditor .jp-Toolbar-item {
  129. margin-top: 2px;
  130. }
  131. #setting-editor .jp-SettingsRawEditor.jp-mod-error .jp-Toolbar-item.jp-BugIcon::after {
  132. color: red;
  133. content: "\25CF"; /* Unicode circle character (error dot) */
  134. font-size: 7px;
  135. width: 100%;
  136. height: 100%;
  137. position: absolute;
  138. top: 4px;
  139. left: 6px;
  140. }
  141. #setting-editor .jp-SettingsRawEditor .jp-Inspector {
  142. border-top: 2px solid var(--jp-layout-color2);
  143. max-height: var(--jp-private-settingeditor-debug-height);
  144. }
  145. #setting-editor .jp-SettingsRawEditor .jp-InspectorItem.jp-SettingsDebug .jp-RenderedHTMLCommon {
  146. padding: 2px 5px 2px 0;
  147. width: 100%;
  148. }
  149. #setting-editor .jp-SettingsRawEditor .jp-InspectorItem.jp-SettingsDebug .jp-RenderedHTMLCommon p {
  150. text-align: right;
  151. }
  152. #setting-editor .jp-SettingsTableEditor {
  153. border: 1px solid var(--jp-brand-color1);
  154. margin: 0;
  155. padding: 0;
  156. }
  157. #setting-editor .jp-SettingsTableEditor legend {
  158. color: var(--jp-brand-color1);
  159. font-size: 70%;
  160. font-weight: bold;
  161. margin-left: 15px;
  162. height: var(--jp-private-settingeditor-legend-height);
  163. }
  164. #setting-editor .jp-SettingsTableEditor-wrapper {
  165. position: absolute;
  166. top: var(--jp-private-settingeditor-legend-height);
  167. bottom: 0;
  168. overflow-y: auto;
  169. }
  170. #setting-editor .jp-SettingsTableEditor table {
  171. table-layout: fixed;
  172. color: var(--jp-ui-font-color1);
  173. font-size: var(--jp-ui-font-size1);
  174. padding: 2px;
  175. width: calc(100% - 4px);
  176. overflow: hidden;
  177. }
  178. #setting-editor .jp-SettingsTableEditor tr {
  179. color: var(--jp-ui-font-color2);
  180. height: var( --jp-private-settingeditor-row-height);
  181. overflow: hidden;
  182. }
  183. #setting-editor .jp-SettingsTableEditor th {
  184. background-color: var(--jp-layout-color3);
  185. border: 1px solid transparent;
  186. font-weight: bold;
  187. height: var( --jp-private-settingeditor-row-height);
  188. }
  189. #setting-editor .jp-SettingsTableEditor td {
  190. border: 1px solid transparent;
  191. height: var( --jp-private-settingeditor-row-height);
  192. }
  193. #setting-editor .jp-SettingsTableEditor th.jp-SettingsTableEditor-key {
  194. width: var(--jp-private-settingeditor-key-width);
  195. }
  196. #setting-editor .jp-SettingsTableEditor th.jp-SettingsTableEditor-type {
  197. width: var(--jp-private-settingeditor-type-width);
  198. }
  199. #setting-editor .jp-SettingsTableEditor td.jp-SettingsTableEditor-key {
  200. overflow: hidden;
  201. white-space: nowrap;
  202. text-overflow: ellipsis;
  203. }
  204. #setting-editor .jp-SettingsTableEditor td.jp-SettingsTableEditor-value {
  205. overflow: hidden;
  206. white-space: nowrap;
  207. text-overflow: ellipsis;
  208. }
  209. #setting-editor .jp-SettingsTableEditor td.jp-SettingsTableEditor-type {
  210. text-align: right;
  211. }